From 919c1e60117fc21acdb66b869a72e44c54c1aaf3 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 29 Oct 2019 14:35:26 -0500 Subject: [PATCH] fix: only push atoms that don't have a value into `next_decisions` --- src/core/Internal.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 749626d2..36d9c24d 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -246,6 +246,7 @@ module Make(Plugin : PLUGIN) let[@inline] id a = a.aid let[@inline] is_true a = a.is_true let[@inline] is_false a = a.neg.is_true + let has_value a = is_true a || is_false a let[@inline] seen a = if sign a @@ -1700,8 +1701,10 @@ module Make(Plugin : PLUGIN) let acts_add_decision_lit (st:t) (f:formula) : unit = let a = create_atom st f in - Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); - st.next_decisions <- a :: st.next_decisions + if not (Atom.has_value a) then ( + Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); + st.next_decisions <- a :: st.next_decisions + ) let acts_raise st (l:formula list) proof : 'a = let atoms = List.rev_map (create_atom st) l in