From 9a5c23d9c53c426d57176cb376a00098737e8b93 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 4 Mar 2016 16:30:51 +0100
Subject: [PATCH] [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     | 36 +++++++++++++++++++-----------------
 solver/solver_types.ml |  1 -
 util/iheap.ml          |  1 +
 util/log.ml            |  2 +-
 4 files changed, 21 insertions(+), 19 deletions(-)

diff --git a/solver/internal.ml b/solver/internal.ml
index bbdf53dd..4b1d7082 100644
--- a/solver/internal.ml
+++ b/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
-        | Either.Left l ->
-          if l.l_level >= 0 then
-            pick_branch_lit ()
-          else begin
-            let value = Th.assign l.term in
-            env.decisions <- env.decisions + 1;
-            new_decision_level();
-            let current_level = decision_level () in
-            enqueue_assign l value current_level
+      begin try
+          begin match St.get_elt (Iheap.remove_min f_weight env.order) with
+            | Either.Left l ->
+              if l.l_level >= 0 then
+                pick_branch_lit ()
+              else begin
+                let value = Th.assign l.term in
+                env.decisions <- env.decisions + 1;
+                new_decision_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 ->
-          pick_branch_aux v.pa
+        with Not_found -> raise Sat
       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 &&
-                    env.elt_head = Vec.size env.elt_queue then
+            else if env.elt_head = Vec.size env.elt_queue (* sanity check *)
+                 && env.elt_head = St.nb_elt () (* this is the important test to know if the search is finished *)  then
               raise Sat
         end
       done
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 261506bb..6c176b7c 100644
--- a/solver/solver_types.ml
+++ b/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
diff --git a/util/iheap.ml b/util/iheap.ml
index f09df933..a0e6603f 100644
--- a/util/iheap.ml
+++ b/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
+
diff --git a/util/log.ml b/util/log.ml
index 58df3ad5..e4261c8e 120000
--- a/util/log.ml
+++ b/util/log.ml
@@ -1 +1 @@
-log_dummy.ml
\ No newline at end of file
+log_real.ml
\ No newline at end of file