mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-01-30 02:09:26 -08:00
commit dadcc6e8ff
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_solver.cpp
View file

@ -122,7 +122,8 @@ namespace smt {
SASSERT(n <= lvl); SASSERT(n <= lvl);
unsigned new_lvl = lvl - n; unsigned new_lvl = lvl - n;
unsigned old_sz = m_scopes[new_lvl]; unsigned old_sz = m_scopes[new_lvl];
for (unsigned i = cur_sz - 1; i >= old_sz; i--) { for (unsigned i = cur_sz; i > old_sz; ) {
--i;
expr * key = m_assumptions[i].get(); expr * key = m_assumptions[i].get();
SASSERT(m_name2assertion.contains(key)); SASSERT(m_name2assertion.contains(key));
expr * value = m_name2assertion.find(key); expr * value = m_name2assertion.find(key);