From fae9481308040ba84fe0e081e142cb9cd3e86cb9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2020 12:17:41 -0800 Subject: [PATCH] fix #4875 remove unsound rewrite, regression --- src/ast/rewriter/seq_rewriter.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0c581b29681..6b024e24343 100644 --- 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; }