diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index d2368cd7..9df6cd9f 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -370,7 +370,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
                                     var_bump_activity a.var;
                                     history := d :: !history;
                                     c := res
-                            | _ -> assert false
+                            | _ ->
+                                L.debug 0 "Found %d resolution lits" (List.length tmp);
+                                List.iter (fun c -> L.debug 0 " |- %a" St.pp_atom c) tmp;
+                                assert false
                             end
                     | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a
                     | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a)