diff --git a/solver/mcproof.ml b/solver/mcproof.ml
index bd440a50..be90ae86 100644
--- a/solver/mcproof.ml
+++ b/solver/mcproof.ml
@@ -80,7 +80,7 @@ module Make(St : Mcsolver_types.S) = struct
     done;
     let l, res = resolve (List.sort_uniq compare_atoms !l) in
     if l <> [] then
-      raise (Resolution_error "Input cause is a tautology");
+      raise (Resolution_error "Input clause is a tautology");
     res
 
   (* Adding hyptoheses *)
diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index d2368cd7..c9c17a2f 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -436,7 +436,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
       | fuip :: _ ->
         let name = fresh_lname () in
         let lclause = make_clause name learnt (List.length learnt) true history in
-        L.debug 1 "New clause learnt : %a" St.pp_clause lclause;
+        L.debug 2 "New clause learnt : %a" St.pp_clause lclause;
         Vec.push env.learnts lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
@@ -632,7 +632,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
     add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma)
 
   let slice_propagate f lvl =
-    enqueue_bool (add_atom f) lvl (Semantic lvl)
+    let a = add_atom f in
+    Iheap.grow_to_by_double env.order (St.nb_vars ());
+    enqueue_bool a lvl (Semantic lvl)
 
   let current_slice () = Th.({
       start = env.tatoms_qhead;