diff --git a/smt/mcsat.ml b/smt/mcsat.ml
index 2ed2022a..425c5ea3 100644
--- a/smt/mcsat.ml
+++ b/smt/mcsat.ml
@@ -18,7 +18,7 @@ module Tsmt = struct
   type proof = unit
 
   let proof_debug () =
-      "Proof", ["..."], Some "PURPLE"
+      "Proof", [], ["..."], Some "PURPLE"
 
   type assumption =
     | Lit of formula
diff --git a/solver/mcproof.ml b/solver/mcproof.ml
index 8798cbb1..6e174359 100644
--- a/solver/mcproof.ml
+++ b/solver/mcproof.ml
@@ -347,13 +347,13 @@ module Make(St : Mcsolver_types.S) = struct
         in
         print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
       | Lemma proof ->
-        let name, args, color = St.proof_debug proof in
-        assert (args <> []);
+        let name, f_args, t_args, color = St.proof_debug proof in
         let color = match color with None -> "YELLOW" | Some c -> c in
         let aux fmt () =
-          Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>%a</TR>"
-            print_clause p.conclusion color (List.length args) name
-            (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TD>%a</TD>" St.print_semantic_var v)) args
+          Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>%a%a</TR>"
+            print_clause p.conclusion color (List.length f_args + List.length t_args) name
+            (fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TD>%a</TD>" St.print_atom a)) f_args
+            (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TD>%a</TD>" St.print_semantic_var v)) t_args
         in
         print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
       | Resolution (proof1, proof2, a) ->
diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml
index 3ea2f83f..7fb77417 100644
--- a/solver/mcsolver_types.ml
+++ b/solver/mcsolver_types.ml
@@ -214,8 +214,8 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
 
   (* Proof debug info *)
   let proof_debug p =
-      let name, l, color = Th.proof_debug p in
-      name, (List.map add_term l), color
+      let name, l, l', color = Th.proof_debug p in
+      name, (List.map add_atom l), (List.map add_term l'), color
 
   (* Pretty printing for atoms and clauses *)
   let print_semantic_var fmt v = E.Term.print fmt v.tag.term
diff --git a/solver/mcsolver_types_intf.ml b/solver/mcsolver_types_intf.ml
index 10d504e5..f2c8e4b6 100644
--- a/solver/mcsolver_types_intf.ml
+++ b/solver/mcsolver_types_intf.ml
@@ -96,7 +96,7 @@ module type S = sig
   val fresh_dname : unit -> string
   (** Fresh names for clauses *)
 
-  val proof_debug : proof -> string * (semantic var list) * (string option)
+  val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option)
   (** Debugging info for proofs (see Plugin_intf). *)
 
   val print_atom : Format.formatter -> atom -> unit
diff --git a/solver/plugin_intf.ml b/solver/plugin_intf.ml
index 65e46908..acf662df 100644
--- a/solver/plugin_intf.ml
+++ b/solver/plugin_intf.ml
@@ -78,7 +78,7 @@ module type S = sig
   val eval : formula -> eval_res
   (** Returns the evaluation of the formula in the current assignment *)
 
-  val proof_debug : proof -> string * (term list) * (string option)
+  val proof_debug : proof -> string * (formula list) * (term list) * (string option)
   (** Returns debugging information on a proof, as a triplet consisting of
       a name/identification string associated with the proof, arguments of the proof,
       and an optional color for the proof background *)