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

Hopefully a fix for restarts

Browse source
This commit is contained in:
Guillaume Bury 2015-03-15 21:32:07 +01:00
parent 582530b9ee
commit 1f0fdf65fd
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
solver/mcsolver.ml
View file

@ -839,14 +839,14 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
begin try
search (to_int !n_of_conflicts) (to_int !n_of_learnts);
with
| Restart -> ()
| Restart ->
n_of_conflicts := !n_of_conflicts *. env.restart_inc;
n_of_learnts := !n_of_learnts *. env.learntsize_inc
| Sat ->
let tag = ref false in
Th.if_sat (full_slice tag);
if not !tag then raise Sat
end;
n_of_conflicts := !n_of_conflicts *. env.restart_inc;
n_of_learnts := !n_of_learnts *. env.learntsize_inc;
end
done;
with
| Sat -> ()