Strings: Remove redundant replace rewrite (#2822)

Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.

1 files changed, 0 insertions, 13 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 8e5e22d38..0c8d6ac8d 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2373,19 +2373,6 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       {
         return returnRewrite(node, node[0], "rpl-const-nfind");
       }
-      // if no overlap, we can pull the first child
-      if (s.overlap(t) == 0)
-      {
-        std::vector<Node> spl(children0.begin() + 1, children0.end());
-        Node ret = NodeManager::currentNM()->mkNode(
-            kind::STRING_CONCAT,
-            children0[0],
-            NodeManager::currentNM()->mkNode(kind::STRING_STRREPL,
-                                             mkConcat(kind::STRING_CONCAT, spl),
-                                             node[1],
-                                             node[2]));
-        return returnRewrite(node, ret, "rpl-prefix-nfind");
-      }
     }
     else
     {