fix #4875

remove unsound rewrite, regression
Z3Prover · Dec 8, 2020 · fae9481 · fae9481
1 parent 97683bd
commit fae9481
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
@@ -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;
 }