[bugfix] some late unsat conflicts were not handled correctly

solver/mcsolver.ml

@@ -454,7 +454,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
 
   let add_boolean_conflict confl =
     env.conflicts <- env.conflicts + 1;
-    if decision_level() = 0 then report_unsat confl; (* Top-level conflict *)
+    if decision_level() = 0 || Vec.for_all (fun a -> a.var.level = 0) confl.atoms then
+        report_unsat confl; (* Top-level conflict *)
     let blevel, learnt, history, is_uip = analyze confl in
     cancel_until blevel;
     record_learnt_clause confl blevel learnt (History history) is_uip

util/vec.ml

@@ -147,6 +147,14 @@ let exists p t =
     false
   with ExitVec -> true
 
+let for_all p t =
+  try
+    for i = 0 to t.sz - 1 do
+      if not (p (Array.unsafe_get t.data i)) then raise ExitVec
+    done;
+    true
+  with ExitVec -> false
+
 (*
 template<class V, class T>
 static inline void remove(V& ts, const T& t)

util/vec.mli

@@ -96,3 +96,6 @@ val fold : ('b -> 'a -> 'b) -> 'b -> 'a t -> 'b
 val exists : ('a -> bool) -> 'a t -> bool
 (** Does there exist an element that satisfies the predicate? *)
 
+val for_all : ('a -> bool) -> 'a t -> bool
+(** Do all elements satisfy the predicate? *)
+