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

fix(sat): fix bug in restarts, we need to solve again after one

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 18:08:42 -05:00
parent ca531d73a6
commit dd58fa21ef
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/Internal.ml
View file

@ -1529,7 +1529,8 @@ module Make (Th : Theory_intf.S) = struct
| exception Restart -> | exception Restart ->
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;
check_invariants st check_invariants st;
call_solve()
| exception Conflict c -> | exception Conflict c ->
add_boolean_conflict st c; add_boolean_conflict st c;
call_solve() call_solve()