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

fix overflow exposed in #880

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-27 09:47:18 -08:00
parent 962979b09c
commit b70f1f0319
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);
unsigned new_lvl = lvl - n;
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();
SASSERT(m_name2assertion.contains(key));
expr * value = m_name2assertion.find(key);