mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
bail out on failure to properly project. issue #837
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
20790c46ee
commit
ff46a925a2
|
@ -909,7 +909,7 @@ namespace qe {
|
|||
num_scopes = 2;
|
||||
}
|
||||
else {
|
||||
if (level.max() + 2 > m_level) return false;
|
||||
if (level.max() + 2 > m_level) return false;
|
||||
SASSERT(level.max() + 2 <= m_level);
|
||||
num_scopes = m_level - level.max();
|
||||
SASSERT(num_scopes >= 2);
|
||||
|
|
Loading…
Reference in a new issue