From 650ea7b9ccd25c1ec3e372baae944a9a0faa73ba Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 11 Jan 2017 18:40:11 +0000 Subject: [PATCH] Bugfix for smt.core.extend_patterns --- src/smt/smt_solver.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 703e4489e..c843c2f78 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -103,6 +103,7 @@ namespace smt { virtual void assert_expr(expr * t, expr * a) { solver_na2as::assert_expr(t, a); + SASSERT(!m_name2assertion.contains(a)); get_manager().inc_ref(t); m_name2assertion.insert(a, t); } @@ -112,6 +113,17 @@ 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); + } m_context.pop(n); } @@ -274,6 +286,7 @@ namespace smt { unsigned sz = core.size(); for (unsigned i = 0; i < sz; i++) { expr_ref name(core[i], m); + SASSERT(m_name2assertion.contains(name)); expr_ref assrtn(m_name2assertion.find(name), m); collect_pattern_func_decls(assrtn, pattern_fds); }