mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fixups wip

Browse source
This commit is contained in:
Murphy Berzish 2016-07-08 12:21:11 -04:00
parent 847a5fc1f8
commit 8aa6fee0af
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str.cpp
View file

@ -141,6 +141,10 @@ void theory_str::assert_axiom(expr * e) {
literal lit(ctx.get_literal(e)); literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit); ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit); ctx.mk_th_axiom(get_id(), 1, &lit);
// crash/error avoidance: add all axioms to the trail
m_trail.push_back(e);
TRACE("t_str_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); TRACE("t_str_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
} }
@ -4622,6 +4626,7 @@ void theory_str::pop_scope_eh(unsigned num_scopes) {
unsigned count = 0; unsigned count = 0;
std::set<expr*> vars = it->second; std::set<expr*> vars = it->second;
for (std::set<expr*>::iterator var_it = vars.begin(); var_it != vars.end(); ++var_it) { for (std::set<expr*>::iterator var_it = vars.begin(); var_it != vars.end(); ++var_it) {
TRACE("t_str_detail", tout << "clean up variable " << mk_pp(*var_it, get_manager()) << std::endl;);
variable_set.erase(*var_it); variable_set.erase(*var_it);
internal_variable_set.erase(*var_it); internal_variable_set.erase(*var_it);
regex_variable_set.erase(*var_it); regex_variable_set.erase(*var_it);