diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 34ac58d18..dbf5d2f38 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6485,7 +6485,7 @@ void theory_str::push_scope_eh() { sLevel += 1; TRACE("t_str", tout << "push to " << sLevel << std::endl;); - TRACE("t_str_dump_assign_on_scope_change", dump_assignments();); + TRACE_CODE(dump_assignments();); } void theory_str::recursive_check_variable_scope(expr * ex) { @@ -6544,7 +6544,7 @@ 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;); - TRACE("t_str_dump_assign_on_scope_change", dump_assignments();); + TRACE_CODE(dump_assignments();); // list of expr* to remove from cut_var_map ptr_vector cutvarmap_removes; @@ -6615,7 +6615,7 @@ void theory_str::pop_scope_eh(unsigned num_scopes) { void theory_str::dump_assignments() { ast_manager & m = get_manager(); context & ctx = get_context(); - TRACE("t_str_detail", + TRACE("t_str_dump_assign_on_scope_change", tout << "dumping all assignments:" << std::endl; expr_ref_vector assignments(m); ctx.get_assignments(assignments); @@ -7503,7 +7503,7 @@ final_check_status theory_str::final_check_eh() { } TRACE("t_str", tout << "final check" << std::endl;); - TRACE("t_str_dump_assign", dump_assignments();); + TRACE_CODE(dump_assignments();); check_variable_scope(); if (opt_DeferEQCConsistencyCheck) {