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

#7391

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-09-22 19:35:03 +01:00
parent a9f8ec1bcb
commit 96c1375786
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -2060,6 +2060,10 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c); result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c);
return BR_REWRITE2; return BR_REWRITE2;
} }
if (str().is_empty(a) && str().is_empty(c)) {
result = a;
return BR_DONE;
}
zstring s1, s2; zstring s1, s2;
expr_ref_vector strs(m()); expr_ref_vector strs(m());
if (str().is_string(a, s1) && str().is_string(b, s2)) { if (str().is_string(a, s1) && str().is_string(b, s2)) {