From db042f7b884ba4475011f9229dd40ff8c2fd2883 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 24 Mar 2021 11:28:02 -0400 Subject: [PATCH] fix: termination issue when using `add_decision_lit` --- src/core/Internal.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 65a5c678..cee6eae4 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1991,7 +1991,6 @@ module Make(Plugin : PLUGIN) | None -> (* No Conflict *) assert (st.elt_head = Vec.size st.trail); assert (st.elt_head = st.th_head); - if Vec.size st.trail = nb_elt st.st then raise_notrace E_sat; if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then ( Log.debug info "(sat.restarting)"; cancel_until st 0; @@ -2047,7 +2046,9 @@ module Make(Plugin : PLUGIN) n_of_conflicts := !n_of_conflicts *. restart_inc; n_of_learnts := !n_of_learnts *. learntsize_inc | E_sat -> - assert (st.elt_head = Vec.size st.trail); + assert (st.elt_head = Vec.size st.trail && + Vec.is_empty st.clauses_to_add && + st.next_decisions=[]); begin match Plugin.final_check st.th (full_slice st) with | () -> if st.elt_head = Vec.size st.trail &&