mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

Bugfix for smt.core.extend_patterns

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-01-11 18:40:11 +00:00
parent 9f49905582
commit 650ea7b9cc
1 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/smt_solver.cpp
View file

@ -103,6 +103,7 @@ namespace smt {
virtual void assert_expr(expr * t, expr * a) { virtual void assert_expr(expr * t, expr * a) {
solver_na2as::assert_expr(t, a); solver_na2as::assert_expr(t, a);
SASSERT(!m_name2assertion.contains(a));
get_manager().inc_ref(t); get_manager().inc_ref(t);
m_name2assertion.insert(a, t); m_name2assertion.insert(a, t);
} }
@ -112,6 +113,17 @@ namespace smt {
} }
virtual void pop_core(unsigned n) { 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); m_context.pop(n);
} }
@ -274,6 +286,7 @@ namespace smt {
unsigned sz = core.size(); unsigned sz = core.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
expr_ref name(core[i], m); expr_ref name(core[i], m);
SASSERT(m_name2assertion.contains(name));
expr_ref assrtn(m_name2assertion.find(name), m); expr_ref assrtn(m_name2assertion.find(name), m);
collect_pattern_func_decls(assrtn, pattern_fds); collect_pattern_func_decls(assrtn, pattern_fds);
} }