mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix #1177

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-31 09:13:50 -07:00
parent 27114ce9dd
commit 8bd0407adf
2 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_context.cpp
View file

@ -2406,7 +2406,7 @@ namespace smt {
if (m_manager.has_trace_stream()) if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
TRACE("context", tout << "backtracking: " << num_scopes << "\n";); TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
TRACE("pop_scope_detail", display(tout);); TRACE("pop_scope_detail", display(tout););
SASSERT(num_scopes > 0); SASSERT(num_scopes > 0);
SASSERT(num_scopes <= m_scope_lvl); SASSERT(num_scopes <= m_scope_lvl);
@ -2901,10 +2901,10 @@ namespace smt {
} }
push_scope(); push_scope();
m_base_scopes.push_back(base_scope()); m_base_scopes.push_back(base_scope());
base_scope & bs = m_base_scopes.back(); base_scope & bs = m_base_scopes.back();
bs.m_lemmas_lim = m_lemmas.size(); bs.m_lemmas_lim = m_lemmas.size();
bs.m_inconsistent = inconsistent(); bs.m_inconsistent = inconsistent();
bs.m_simp_qhead_lim = m_simp_qhead; bs.m_simp_qhead_lim = m_simp_qhead;
m_base_lvl++; m_base_lvl++;
m_search_lvl++; // Not really necessary. But, it is useful to enforce the invariant m_search_lvl >= m_base_lvl m_search_lvl++; // Not really necessary. But, it is useful to enforce the invariant m_search_lvl >= m_base_lvl
SASSERT(m_base_lvl <= m_scope_lvl); SASSERT(m_base_lvl <= m_scope_lvl);
@ -2912,6 +2912,7 @@ namespace smt {
void context::pop(unsigned num_scopes) { void context::pop(unsigned num_scopes) {
SASSERT (num_scopes > 0); SASSERT (num_scopes > 0);
if (num_scopes > m_scope_lvl) return;
pop_to_base_lvl(); pop_to_base_lvl();
pop_scope(num_scopes); pop_scope(num_scopes);
} }

1
src/smt/smt_justification.h
View file

@ -148,6 +148,7 @@ namespace smt {
m_node1(n1), m_node1(n1),
m_node2(n2), m_node2(n2),
m_js(js) { m_js(js) {
SASSERT(n1 != n2);
} }
virtual void get_antecedents(conflict_resolution & cr); virtual void get_antecedents(conflict_resolution & cr);