mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

explicitly re-introduce string axioms on refreshed string theory vars

Browse source 
this fixes at least one case (kaluza/unsat/big/9650.smt2) where a string
could have a negative length value due to a constraint that went out of scope
This commit is contained in:
Murphy Berzish 2016-12-09 17:12:29 -05:00
parent 737565180f
commit e9411e5b8c
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str.cpp
View file

@ -320,6 +320,9 @@ void theory_str::refresh_theory_var(expr * e) {
enode * en = ensure_enode(e);
theory_var v = mk_var(en);
TRACE("t_str_detail", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;);
// TODO this is probably sub-optimal
// TODO case where the refreshed var must be non-empty?
m_basicstr_axiom_todo.push_back(en);
}
theory_var theory_str::mk_var(enode* n) {