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

fix #5061

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-03 11:19:03 -08:00
parent 8c66691e6d
commit 11efe33aa0
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2009,8 +2009,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
}
expr* b2 = nullptr, *b3 = nullptr;
if (str().is_replace(b, b1, b2, b3) && b2 == a1 && str().is_empty(b3)) {
result = str().mk_prefix(str().mk_concat(a1, a1), b1);
if (str().is_replace(b, b1, b2, b3) && b2 == a && str().is_empty(b3)) {
result = str().mk_prefix(str().mk_concat(a, a), b1);
return BR_REWRITE2;
}