From 46ff8c3ba69105b488fd77e47bff28209354036e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 18 Aug 2018 17:20:20 -0500 Subject: [PATCH] fix(sat): bug with re-internalization of terms upon backtracking --- src/sat/Internal.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/sat/Internal.ml b/src/sat/Internal.ml index c09776f1..2d3fd375 100644 --- a/src/sat/Internal.ml +++ b/src/sat/Internal.ml @@ -769,12 +769,13 @@ module Make (Th : Theory_intf.S) = struct if not (Var.in_heap v) && Var.level v < 0 then ( (* new variable that is not assigned, add to heap and to theory. *) H.insert st.order v; - Th.add_formula (Lazy.force st.th) v.v_pa.lit; - Th.add_formula (Lazy.force st.th) v.v_na.lit; ) (* attach an atom by deciding on its variable, if needed *) - let[@inline] attach_atom (st:t) (a:atom) : unit = insert_var_order st a.var + let attach_atom (st:t) (a:atom) : unit = + insert_var_order st a.var; + Th.add_formula (Lazy.force st.th) a.lit; + Th.add_formula (Lazy.force st.th) a.neg.lit (* Rather than iterate over all the heap when we want to decrease all the variables/literals activity, we instead increase the value by which @@ -1557,6 +1558,7 @@ module Make (Th : Theory_intf.S) = struct call_solve() | exception Sat -> assert (st.elt_head = Vec.size st.trail); + check_invariants st; begin match Th.if_sat (theory st) (full_slice st) with | Theory_intf.Sat -> (* if no propagation is to be done, exit;