mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-12 02:04:43 +00:00
Code Activity

fix #4079

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-23 22:35:33 -07:00
parent 64cb5cad81
commit eb2d7d3e81
3 changed files with 19 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.cpp
View file

@ -1891,7 +1891,7 @@ namespace smt {
m_region.push_scope();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
TRACE("context", tout << "push " << m_scope_lvl << "\n";);
// TRACE("context", tout << "push " << m_scope_lvl << "\n";);
m_relevancy_propagator->push();
s.m_assigned_literals_lim = m_assigned_literals.size();
@ -2335,7 +2335,7 @@ namespace smt {
if (m.has_trace_stream() && !m_is_auxiliary)
m.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
// TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
TRACE("pop_scope_detail", display(tout););
SASSERT(num_scopes > 0);
SASSERT(num_scopes <= m_scope_lvl);