diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index f9ab63ba..6d0d51ae 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -612,10 +612,11 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
 
   (* Propagation (boolean and theory) *)
   let new_atom f =
-      let a = add_atom f in
-      L.debug 10 "New atom : %a" St.pp_atom a;
-      ignore (th_eval a);
-      a
+    L.debug 100 "New_atom";
+    let a = add_atom f in
+    L.debug 10 "New atom : %a" St.pp_atom a;
+    ignore (th_eval a);
+    a
 
   let slice_get i = Either.destruct (Vec.get env.trail i)
       (function {level; tag={term; assigned = Some v}} -> Th.Assign (term, v), level | _ -> assert false)
diff --git a/solver/mcsolver_types.ml b/solver/mcsolver_types.ml
index 87071248..d5d1942a 100644
--- a/solver/mcsolver_types.ml
+++ b/solver/mcsolver_types.ml
@@ -172,9 +172,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
   let add_term t = make_semantic_var t
 
   let add_atom lit =
-    Log.debug 100 "entering add_atom";
+    L.debug 100 "entering add_atom";
     let var, negated = make_boolean_var lit in
-    Log.debug 100 "found atom";
+    L.debug 100 "found atom";
     if negated then var.tag.na else var.tag.pa
 
   let make_clause name ali sz_ali is_learnt premise =