simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: termination issue when using add_decision_lit

Browse source
This commit is contained in:
Simon Cruanes 2021-03-24 11:28:02 -04:00
parent a64202c6ec
commit db042f7b88
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/core/Internal.ml
View file

@ -1991,7 +1991,6 @@ module Make(Plugin : PLUGIN)
| None -> (* No Conflict *) | None -> (* No Conflict *)
assert (st.elt_head = Vec.size st.trail); assert (st.elt_head = Vec.size st.trail);
assert (st.elt_head = st.th_head); 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 ( if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then (
Log.debug info "(sat.restarting)"; Log.debug info "(sat.restarting)";
cancel_until st 0; cancel_until st 0;
@ -2047,7 +2046,9 @@ module Make(Plugin : PLUGIN)
n_of_conflicts := !n_of_conflicts *. restart_inc; n_of_conflicts := !n_of_conflicts *. restart_inc;
n_of_learnts := !n_of_learnts *. learntsize_inc n_of_learnts := !n_of_learnts *. learntsize_inc
| E_sat -> | 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 begin match Plugin.final_check st.th (full_slice st) with
| () -> | () ->
if st.elt_head = Vec.size st.trail && if st.elt_head = Vec.size st.trail &&