From 8776b97841c80e476bf18dc32304c6efb5146050 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 14 Sep 2016 22:08:40 -0400 Subject: [PATCH] variable scope correctness hack in theory_str --- src/smt/theory_str.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1dcfb0b29..d73d55dc3 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6483,6 +6483,12 @@ void theory_str::push_scope_eh() { theory::push_scope_eh(); m_trail_stack.push_scope(); + // TODO out-of-scope term debugging, see comment in pop_scope_eh() + context & ctx = get_context(); + ast_manager & m = get_manager(); + expr_ref_vector assignments(m); + ctx.get_assignments(assignments); + sLevel += 1; TRACE("t_str", tout << "push to " << sLevel << std::endl;); TRACE_CODE(dump_assignments();); @@ -6544,6 +6550,12 @@ void theory_str::check_variable_scope() { void theory_str::pop_scope_eh(unsigned num_scopes) { sLevel -= num_scopes; TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); + // TODO: figure out what's going out of scope and why + context & ctx = get_context(); + ast_manager & m = get_manager(); + expr_ref_vector assignments(m); + ctx.get_assignments(assignments); + TRACE_CODE(dump_assignments();); // list of expr* to remove from cut_var_map @@ -7500,6 +7512,10 @@ final_check_status theory_str::final_check_eh() { context & ctx = get_context(); ast_manager & m = get_manager(); + // TODO out-of-scope term debugging, see comment in pop_scope_eh() + expr_ref_vector assignments(m); + ctx.get_assignments(assignments); + if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = false; }