mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix #4875

Browse source 
remove unsound rewrite, regression
This commit is contained in:
Nikolaj Bjorner 2020-12-08 12:17:41 -08:00
parent 97683bd48a
commit fae9481308
1 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1685,12 +1685,6 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
return BR_REWRITE_FULL;
}
expr* a1 = nullptr, *b1 = nullptr, *c1 = nullptr;
if (str().is_replace(a, a1, b1, c1) && c1 == b && c1 != c) {
result = str().mk_replace(a1, b1, c);
result = str().mk_replace(result, b, c);
return BR_REWRITE2;
}
return BR_FAILED;
}