[bugfix] termination check after full slice was wrong

When the solver finds a SAT result, it sends the whole
model to the theory, because maybe it can do something
interesting/costly to expand the proof search. After
that there must be a check to see if the theory has effectively done
something, in which case we should resume proof search, or if nothing
has been done, in which case the solver should return that the problem
is satisfiable. That check was incorrect before (checking number of
assumptions, and if the queue is all caught up), because new learnt
clauses (i.e tautologies, which are *not* assumptions) can be added that
do not immediately causes propagation, so that the number of assumptions
and the element queue is constant, but we should still resume the
search.

solver/internal.ml

@@ -898,32 +898,35 @@ module Make
       env.next_decision <- None;
       pick_branch_aux atom
     | None ->
-      begin match St.get_elt (Iheap.remove_min f_weight env.order) with
+      begin try
-        | Either.Left l ->
+          begin match St.get_elt (Iheap.remove_min f_weight env.order) with
-          if l.l_level >= 0 then
+            | Either.Left l ->
-            pick_branch_lit ()
+              if l.l_level >= 0 then
-          else begin
+                pick_branch_lit ()
-            let value = Th.assign l.term in
+              else begin
-            env.decisions <- env.decisions + 1;
+                let value = Th.assign l.term in
-            new_decision_level();
+                env.decisions <- env.decisions + 1;
-            let current_level = decision_level () in
+                new_decision_level();
-            enqueue_assign l value current_level
+                let current_level = decision_level () in
+                enqueue_assign l value current_level
+              end
+            | Either.Right v ->
+              pick_branch_aux v.pa
           end
-        | Either.Right v ->
+        with Not_found -> raise Sat
-          pick_branch_aux v.pa
       end
 
-
   let search n_of_conflicts n_of_learnts =
     let conflictC = ref 0 in
     env.starts <- env.starts + 1;
-    while (true) do
+    while true do
       match propagate () with
       | Some confl -> (* Conflict *)
         incr conflictC;
         add_boolean_conflict confl
 
       | None -> (* No Conflict *)
+        assert (env.elt_head = Vec.size env.elt_queue);
         if Vec.size env.elt_queue = St.nb_elt () (* env.nb_init_vars *) then raise Sat;
         if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then begin
           env.progress_estimate <- progress_estimate();
@@ -975,11 +978,10 @@ module Make
             n_of_conflicts := !n_of_conflicts *. env.restart_inc;
             n_of_learnts   := !n_of_learnts *. env.learntsize_inc
           | Sat ->
-            let nbc = env.nb_init_clauses in
             Th.if_sat (full_slice ());
             if is_unsat () then raise Unsat
-            else if env.nb_init_clauses = nbc &&
+            else if env.elt_head = Vec.size env.elt_queue (* sanity check *)
-                    env.elt_head = Vec.size env.elt_queue then
+                 && env.elt_head = St.nb_elt () (* this is the important test to know if the search is finished *)  then
               raise Sat
         end
       done

solver/solver_types.ml

@@ -170,7 +170,6 @@ module McMake (E : Expr_intf.S) = struct
         MF.add f_map lit var;
         incr cpt_mk_var;
         Vec.push vars (Either.mk_right var);
-        (* Th.iter_assignable (fun t -> ignore (make_semantic_var t)) lit; *)
         var, negated
 
   let add_term t = make_semantic_var t

util/iheap.ml

@@ -138,3 +138,4 @@ let remove_min cmp ({heap=heap; indices=indices} as s) =
   Vec.pop s.heap;
   if Vec.size s.heap > 1 then percolate_down cmp s 0;
   x
+

util/log.ml

@@ -1 +1 @@
-log_dummy.ml
+log_real.ml