simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Little test

Browse source
This commit is contained in:
Guillaume Bury 2015-03-16 15:22:18 +01:00
parent 381081314e
commit a362505d86
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

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