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

selective expansion of strings for canonizer to fix #1690 regression

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-18 20:42:53 -07:00
parent 4634d1daed
commit 6a0b70ee5c
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_seq.cpp
View file

@ -2898,14 +2898,13 @@ expr_ref theory_seq::expand(expr* e, dependency*& eqs) {
expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){ expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
expr_ref result(m); expr_ref result(m);
expr_dep ed; expr_dep ed;
zstring s;
if (m_rep.find_cache(e, ed)) { if (m_rep.find_cache(e, ed)) {
if (e != ed.first) { if (e != ed.first) {
eqs = m_dm.mk_join(eqs, ed.second); eqs = m_dm.mk_join(eqs, ed.second);
} }
result = ed.first; result = ed.first;
} }
else if (m_util.str.is_string(e, s) && s.length() > 0) { else if (m_util.str.is_string(e)) {
result = add_elim_string_axiom(e); result = add_elim_string_axiom(e);
} }
else { else {