From 69abe1687e14bbbf5cabe0aebd0909fd7f2b59cf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Sep 2019 20:17:07 -0400 Subject: [PATCH] backjump to level of clause to ensure that new atoms created by projection are assigned as assumptions fix #2557 Signed-off-by: Nikolaj Bjorner --- src/qe/nlqsat.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index a0084e071..b733ef4f2 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -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); }