From 443a3b07313085e02e57c4c3818ee2f7b073c470 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 9 Nov 2016 00:24:41 +0100
Subject: [PATCH] [bugfix] Attempt at fixing enqueue bug

When we enqueue an atom at level 0, we expect it to stay unconditionally
true whatever happens. However, if it happens that the atom is alrady
true at a level strictly greater than 0 (but lower than base_level),
then enqueue_bool would simply do nothing. To fix this, there is a new
function enqueue_root which modifies in place the level and reason of
the propagated atom if it is already true.
Additionally, enqueue_bool now requires that the atom be undecided,
since if it not (i.e if it is propagated while already decided) it is
most likely a bug.
---
 src/core/internal.ml | 39 +++++++++++++++++++++++++--------------
 1 file changed, 25 insertions(+), 14 deletions(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 8a8b22e7..8fea0435 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -473,19 +473,30 @@ module Make
       Log.debugf 0 "Trying to enqueue a false literal: %a" (fun k->k St.pp_atom a);
       assert false
     end;
-    if not a.is_true then begin
-      assert (a.var.v_level < 0 && a.var.reason = None && lvl >= 0);
-      let reason =
-        if lvl > 0 then reason
-        else simpl_reason reason
-      in
-      a.is_true <- true;
-      a.var.v_level <- lvl;
-      a.var.reason <- Some reason;
-      Vec.push env.elt_queue (of_atom a);
-      Log.debugf 20 "Enqueue (%d): %a"
-        (fun k->k (Vec.size env.elt_queue) pp_atom a)
-    end
+    assert (not a.is_true && a.var.v_level < 0 &&
+            a.var.reason = None && lvl >= 0);
+    let reason =
+      if lvl > 0 then reason
+      else simpl_reason reason
+    in
+    a.is_true <- true;
+    a.var.v_level <- lvl;
+    a.var.reason <- Some reason;
+    Vec.push env.elt_queue (of_atom a);
+    Log.debugf 20 "Enqueue (%d): %a"
+      (fun k->k (Vec.size env.elt_queue) pp_atom a)
+
+  (* Special case for atoms enqueued at level 0
+     Indeed atoms true at level 0 are supposed to never disappear, because
+     we cannot watch a clause with only one atom. This causes a problem when
+     the atom [a] is already propagated at a level 0 < l <= base_level
+     In that case, we simply change the level and reason of the propagation. *)
+  let enqueue_root a clause : unit =
+    if a.is_true then begin
+      a.var.v_level <- 0;
+      a.var.reason <- Some (Bcp clause)
+    end else
+      enqueue_bool a ~level:0 (Bcp clause)
 
   (* MCsat semantic assignment *)
   let enqueue_assign l value lvl =
@@ -787,7 +798,7 @@ module Make
           Vec.pop vec;
           report_unsat clause
         end else
-          enqueue_bool a 0 (Bcp clause)
+          enqueue_root a clause
       | a::b::_ ->
         if a.neg.is_true then begin
           (* Atoms need to be sorted in decreasing order of decision level,