Merge branch 'master' into fixStaticInstallfixStaticInstall

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 3c40062f5..befe52574 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -2948,6 +2948,13 @@ Node SequencesRewriter::rewriteReplaceRe(Node node)
       return returnRewrite(node, x, Rewrite::REPLACE_RE_EVAL);
     }
   }
+  // str.replace_re( x, y, z ) ---> z ++ x if "" in y ---> true
+  String emptyStr("");
+  if (RegExpEntail::testConstStringInRegExp(emptyStr, 0, y))
+  {
+    Node ret = nm->mkNode(STRING_CONCAT, z, x);
+    return returnRewrite(node, ret, Rewrite::REPLACE_RE_EMP_RE);
+  }
   return node;
 }