mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

variable scope correctness hack in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-09-14 22:08:40 -04:00
parent bed40c45b8
commit 8776b97841
1 changed files with 16 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_str.cpp
View file

@ -6483,6 +6483,12 @@ void theory_str::push_scope_eh() {
theory::push_scope_eh(); theory::push_scope_eh();
m_trail_stack.push_scope(); 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; sLevel += 1;
TRACE("t_str", tout << "push to " << sLevel << std::endl;); TRACE("t_str", tout << "push to " << sLevel << std::endl;);
TRACE_CODE(dump_assignments();); TRACE_CODE(dump_assignments(););
@ -6544,6 +6550,12 @@ void theory_str::check_variable_scope() {
void theory_str::pop_scope_eh(unsigned num_scopes) { void theory_str::pop_scope_eh(unsigned num_scopes) {
sLevel -= num_scopes; sLevel -= num_scopes;
TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); 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();); TRACE_CODE(dump_assignments(););
// list of expr* to remove from cut_var_map // 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(); context & ctx = get_context();
ast_manager & m = get_manager(); 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) { if (opt_VerifyFinalCheckProgress) {
finalCheckProgressIndicator = false; finalCheckProgressIndicator = false;
} }