mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
backjump to level of clause to ensure that new atoms created by projection are assigned as assumptions fix #2557
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0f20175bdd
commit
69abe1687e
|
@ -475,9 +475,6 @@ namespace qe {
|
|||
else {
|
||||
SASSERT(clevel.max() + 2 <= level());
|
||||
num_scopes = level() - clevel.max();
|
||||
if ((num_scopes % 2) != 0) {
|
||||
--num_scopes;
|
||||
}
|
||||
SASSERT(num_scopes >= 2);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue