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

fix bug

Browse source
This commit is contained in:
Simon Cruanes 2016-07-28 10:18:07 +02:00
parent 2e8b45edbc
commit ac706f3e56
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/core/internal.ml
View file

@ -1134,6 +1134,8 @@ module Make
if is_unsat () then raise Unsat;
let n_of_conflicts = ref (to_float env.restart_first) in
let n_of_learnts = ref ((to_float (nb_clauses())) *. env.learntsize_factor) in
(* return to level 0 before pushing assumptions *)
cancel_until 0;
push_assumptions assumptions;
assert (env.base_level <= List.length assumptions);
try