mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

fix #5117

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-30 14:23:30 -07:00
parent c71bbb6391
commit 1fcd537d81
1 changed files with 0 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2017,11 +2017,6 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
return BR_DONE; return BR_DONE;
} }
expr* b2 = nullptr, *b3 = nullptr;
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;
}
unsigned len_a; unsigned len_a;
rational len_b; rational len_b;