From 3c6da0ffdc0d0f55069ee4186ef6a7e7b0a4c12c Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 26 Jul 2016 14:27:22 +0200 Subject: [PATCH] Clause buffer must be fitered when popping 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. --- src/core/internal.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/core/internal.ml b/src/core/internal.ml index f986ef9a..7bb93c8a 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -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));