From 44509c6f8dd88634b174f6af912ba7637a1b9c63 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 27 Jan 2017 17:56:47 +0100
Subject: [PATCH] [bugfix] conflict in forgetful propagation

---
 src/core/internal.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 2fd8ce5e..0637e034 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -733,7 +733,7 @@ module Make
 
   (* Add a new clause, simplifying, propagating, and backtracking if
      the clause is false in the current trail *)
-  let add_clause ?(force=false) (init:clause) : unit =
+  let add_clause (init:clause) : unit =
     Log.debugf debug "Adding clause: @[<hov>%a@]" (fun k -> k St.pp_clause init);
     let vec = match init.cpremise with
       | Hyp -> env.clauses_hyps
@@ -932,7 +932,11 @@ module Make
         let p = atom f in
         let c = make_clause (fresh_tname ())
             (p :: List.map (fun a -> a.neg) l) (Lemma proof) in
-        enqueue_bool p (decision_level ()) (Bcp c)
+        if p.is_true then ()
+        else if p.neg.is_true then
+          Stack.push c env.clauses_to_add
+        else
+          enqueue_bool p (decision_level ()) (Bcp c)
       else
         raise (Invalid_argument "Msat.Internal.slice_propagate")