diff --git a/sat/sat.ml b/sat/sat.ml
index e7d2fbcb..fe1ed80a 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -141,8 +141,7 @@ module Make(Log : Log_intf.S) = struct
   let eval = SatSolver.eval
 
   let get_proof () =
-    SatSolver.Proof.learn (SatSolver.hyps ());
-    SatSolver.Proof.learn (SatSolver.history ());
+    (* SatSolver.Proof.learn (SatSolver.history ()); *)
     match SatSolver.unsat_conflict () with
     | None -> assert false
     | Some c -> SatSolver.Proof.prove_unsat c
diff --git a/smt/mcsat.ml b/smt/mcsat.ml
index ddde97e7..515181cc 100644
--- a/smt/mcsat.ml
+++ b/smt/mcsat.ml
@@ -135,8 +135,7 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> ()
 
   let get_proof () =
-    SmtSolver.Proof.learn (SmtSolver.hyps ());
-    SmtSolver.Proof.learn (SmtSolver.history ());
+    (* SmtSolver.Proof.learn (SmtSolver.history ()); *)
     match SmtSolver.unsat_conflict () with
     | None -> assert false
     | Some c -> SmtSolver.Proof.prove_unsat c
diff --git a/smt/smt.ml b/smt/smt.ml
index 21cf68b7..68f866da 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -84,8 +84,7 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> ()
 
   let get_proof () =
-    SmtSolver.Proof.learn (SmtSolver.hyps ());
-    SmtSolver.Proof.learn (SmtSolver.history ());
+    (* SmtSolver.Proof.learn (SmtSolver.history ()); *)
     match SmtSolver.unsat_conflict () with
     | None -> assert false
     | Some c -> SmtSolver.Proof.prove_unsat c
diff --git a/solver/mcproof.ml b/solver/mcproof.ml
index 352d373b..a44f0601 100644
--- a/solver/mcproof.ml
+++ b/solver/mcproof.ml
@@ -130,7 +130,15 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct
     | _ ->
       raise (Resolution_error "Could not find a reason needed to resolve")
 
-  let add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
+  let need_clause (c, cl) =
+    if is_proved (c, cl) then
+      []
+    else
+      match St.(c.cpremise) with
+      | St.History l -> l
+      | St.Lemma _ -> assert false
+
+  let rec add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
     match l with
     | a :: r ->
       L.debug 5 "Resolving (with history) %a" St.pp_clause c;
@@ -140,21 +148,14 @@ module Make(L : Log_intf.S)(St : Mcsolver_types.S) = struct
       while not (equal_cl cl !new_cl) do
         let unit_to_use = diff_learnt [] cl !new_cl in
         let unit_r = List.map (fun a -> clause_unit a) unit_to_use in
+        do_clause (List.map fst unit_r);
         let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
         new_c := temp_c;
         new_cl := temp_cl;
       done
     | _ -> assert false
 
-  let need_clause (c, cl) =
-    if is_proved (c, cl) then
-      []
-    else
-      match St.(c.cpremise) with
-      | St.History l -> l
-      | St.Lemma _ -> assert false
-
-  let rec do_clause = function
+  and do_clause = function
     | [] -> ()
     | c :: r ->
       let cl = to_list c in
diff --git a/solver/res.ml b/solver/res.ml
index 68226c13..a068ba1a 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -129,7 +129,15 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     | _ ->
       raise (Resolution_error "Could not find a reason needed to resolve")
 
-  let add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
+  let need_clause (c, cl) =
+    if is_proved (c, cl) then
+      []
+    else
+      match St.(c.cpremise) with
+      | St.History l -> l
+      | St.Lemma _ -> assert false
+
+  let rec add_clause c cl l = (* We assume that all clauses in l are already proved ! *)
     match l with
     | a :: r ->
       L.debug 5 "Resolving (with history) %a" St.pp_clause c;
@@ -139,21 +147,14 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
       while not (equal_cl cl !new_cl) do
         let unit_to_use = diff_learnt [] cl !new_cl in
         let unit_r = List.map (fun a -> clause_unit a) unit_to_use in
+        do_clause (List.map fst unit_r);
         let temp_c, temp_cl = List.fold_left add_res (!new_c, !new_cl) unit_r in
         new_c := temp_c;
         new_cl := temp_cl;
       done
     | _ -> assert false
 
-  let need_clause (c, cl) =
-    if is_proved (c, cl) then
-      []
-    else
-      match St.(c.cpremise) with
-      | St.History l -> l
-      | St.Lemma _ -> assert false
-
-  let rec do_clause = function
+  and do_clause = function
     | [] -> ()
     | c :: r ->
       let cl = to_list c in