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

Clause buffer must be fitered when popping

Browse source 
Indeed imagine the following case:
"push; assume [c]; pop; push; solve"
since c has user-level 1, in the current state, it would
have been wrongfully added to the solver state when solve
is run.
This commit is contained in:
Guillaume Bury 2016-07-26 14:27:22 +02:00
parent defcb67aad
commit 3c6da0ffdc
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core/internal.ml
View file

@ -1229,6 +1229,15 @@ module Make
if l > current_level () then invalid_arg "cannot pop to level, it is too high"
else if l < current_level () then begin
(* Filter the current buffer of clauses to remove potential assumptions
with too high a user level,
or else, with later pushes, these assumptions might be added. *)
let cl = Stack.fold (fun acc c ->
if c.c_level > l then acc else c :: acc) [] env.clauses_to_add in
Stack.clear env.clauses_to_add;
List.iter (fun c -> Stack.push c env.clauses_to_add) cl;
(* Get back the user level *)
let ul = Vec.get env.user_levels l in
Vec.shrink env.user_levels (max 0 (Vec.size env.user_levels - l - 1));