From 2458db30cf0329128db4c92e79909284892619f0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Jan 2017 12:49:26 +0000 Subject: [PATCH] Corner-case fix for smt::solver::pop_core --- src/smt/smt_solver.cpp | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c843c2f78..f80ff09f4 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -113,16 +113,19 @@ namespace smt { } virtual void pop_core(unsigned n) { - unsigned lvl = m_scopes.size(); - SASSERT(n <= lvl); - unsigned new_lvl = lvl - n; - unsigned old_sz = m_scopes[new_lvl]; - for (unsigned i = m_assumptions.size() - 1; i >= old_sz; i--) { - expr * key = m_assumptions[i].get(); - SASSERT(m_name2assertion.contains(key)); - expr * value = m_name2assertion.find(key); - m.dec_ref(value); - m_name2assertion.erase(key); + unsigned cur_sz = m_assumptions.size(); + if (n > 0 && cur_sz > 0) { + unsigned lvl = m_scopes.size(); + 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--) { + expr * key = m_assumptions[i].get(); + SASSERT(m_name2assertion.contains(key)); + expr * value = m_name2assertion.find(key); + m.dec_ref(value); + m_name2assertion.erase(key); + } } m_context.pop(n); }