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

in some case, Solver.pop can reset env.is_unsat

Browse source
This commit is contained in:
Simon Cruanes 2014-11-04 00:16:37 +01:00
parent f18b77cdaa
commit e88eb28049
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
sat/solver.ml
View file

@ -927,6 +927,12 @@ module Make (F : Formula_intf.S)
if l > current_level() if l > current_level()
then invalid_arg "cannot pop() to level, it is too high"; then invalid_arg "cannot pop() to level, it is too high";
let i = Vec.get env.levels l in let i = Vec.get env.levels l in
(* see whether we can reset [env.is_unsat] *)
if env.is_unsat && not (Vec.is_empty env.trail_lim) then (
(* level at which the decision that lead to unsat was made *)
let last = Vec.last env.trail_lim in
if i < last then env.is_unsat <- false
);
cancel_until i cancel_until i
let clear () = pop base_level let clear () = pop base_level