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

fix #5399

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-10 14:47:51 +02:00
parent 2973d3bdc1
commit 0f8d2d1d51
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

@ -1775,6 +1775,10 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
result = str().mk_concat(c, a);
return BR_REWRITE1;
}
if (str().is_empty(a) && str().is_empty(c)) {
result = a;
return BR_DONE;
}
m_lhs.reset();
str().get_concat(a, m_lhs);