mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

fix #2980

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-11 22:43:00 -08:00
parent 4f6e3cfe71
commit bbce6bfa07
1 changed files with 13 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/smt_context.cpp
View file

@ -2383,6 +2383,8 @@ namespace smt {
*/ */
unsigned context::pop_scope_core(unsigned num_scopes) { unsigned context::pop_scope_core(unsigned num_scopes) {
unsigned units_to_reassert_lim;
try { try {
if (m.has_trace_stream() && !m_is_auxiliary) if (m.has_trace_stream() && !m_is_auxiliary)
m.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; m.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
@ -2403,7 +2405,7 @@ namespace smt {
scope & s = m_scopes[new_lvl]; scope & s = m_scopes[new_lvl];
TRACE("context", tout << "backtracking new_lvl: " << new_lvl << "\n";); TRACE("context", tout << "backtracking new_lvl: " << new_lvl << "\n";);
unsigned units_to_reassert_lim = s.m_units_to_reassert_lim; units_to_reassert_lim = s.m_units_to_reassert_lim;
if (new_lvl < m_base_lvl) { if (new_lvl < m_base_lvl) {
base_scope & bs = m_base_scopes[new_lvl]; base_scope & bs = m_base_scopes[new_lvl];
@ -2449,20 +2451,22 @@ namespace smt {
m_base_lvl = new_lvl; m_base_lvl = new_lvl;
m_search_lvl = new_lvl; // Remark: not really necessary m_search_lvl = new_lvl; // Remark: not really necessary
} }
unsigned num_bool_vars = get_num_bool_vars();
// any variable >= num_bool_vars was deleted during backtracking.
reinit_clauses(num_scopes, num_bool_vars);
reassert_units(units_to_reassert_lim);
TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout););
CASSERT("context", check_invariant());
return num_bool_vars;
} }
catch (...) { catch (...) {
// throwing inside pop is just not cool. // throwing inside pop is just not cool.
UNREACHABLE(); UNREACHABLE();
throw; throw;
} }
// an exception can happen when axioms are reinitialized (because they are rewritten).
unsigned num_bool_vars = get_num_bool_vars();
// any variable >= num_bool_vars was deleted during backtracking.
reinit_clauses(num_scopes, num_bool_vars);
reassert_units(units_to_reassert_lim);
TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout););
CASSERT("context", check_invariant());
return num_bool_vars;
} }
void context::pop_scope(unsigned num_scopes) { void context::pop_scope(unsigned num_scopes) {