diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 7a4d2017..06e1b6a8 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -285,7 +285,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
     assert (Vec.size env.trail_lim = Vec.size env.tenv_queue)
 
   let report_unsat ({atoms=atoms} as confl) =
-    L.debug 5 "Unsat conflict : %a" St.pp_clause confl;
+    L.debug 4 "Unsat conflict : %a" St.pp_clause confl;
     env.unsat_conflict <- Some confl;
     env.is_unsat <- true;
     raise Unsat
@@ -299,16 +299,15 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
       a.is_true <- true;
       a.var.level <- lvl;
       a.var.tag.reason <- reason;
-      L.debug 8 "Enqueue: %a" pp_atom a;
+      L.debug 2 "Enqueue: %a" pp_atom a;
       Vec.push env.trail (Either.mk_right a)
     end
 
   let enqueue_assign v value lvl =
     v.tag.assigned <- Some value;
     v.level <- lvl;
-    L.debug 5 "Enqueue: %a" St.pp_semantic_var v;
-    Vec.push env.trail (Either.mk_left v);
-    L.debug 15 "Done."
+    L.debug 2 "Enqueue: %a" St.pp_semantic_var v;
+    Vec.push env.trail (Either.mk_left v)
 
   (* conflict analysis *)
   let max_lvl_atoms l =
@@ -423,13 +422,13 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
         fuip.var.tag.vpremise <- history;
         let name = fresh_lname () in
         let uclause = make_clause name learnt (List.length learnt) true history in
-        L.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
+        L.debug 1 "Unit clause learnt : %a" St.pp_clause uclause;
         Vec.push env.learnts uclause;
         enqueue_bool fuip 0 (Bcp (Some uclause))
       | fuip :: _ ->
         let name = fresh_lname () in
         let lclause = make_clause name learnt (List.length learnt) true history in
-        L.debug 2 "New clause learnt : %a" St.pp_clause lclause;
+        L.debug 1 "New clause learnt : %a" St.pp_clause lclause;
         Vec.push env.learnts lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
@@ -508,7 +507,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
       | a::b::_ ->
         let name = fresh_name () in
         let clause = make_clause name atoms size (history <> History []) history in
-        L.debug 10 "New clause : %a" St.pp_clause init0;
+        L.debug 1 "New clause : %a" St.pp_clause init0;
         attach_clause clause;
         Vec.push env.clauses clause;
         if a.neg.is_true then begin