From aca0cef5cf1bcb882dce927a64917aa800dd8b27 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 30 Jul 2019 09:57:33 -0500
Subject: [PATCH] Minor improvement for rewriter for str.replace (#3124)

---
 src/theory/strings/theory_strings_rewriter.cpp | 18 ++++++++++++------
 test/regress/CMakeLists.txt                    |  1 +
 .../regress0/strings/replace-const.smt2        | 12 ++++++++++++
 3 files changed, 25 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress0/strings/replace-const.smt2

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index d720fedc8..aac2477ea 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2456,14 +2456,20 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     }
     else
     {
-      CVC4::String s1 = s.substr(0, (int)p);
-      CVC4::String s3 = s.substr((int)p + (int)t.size());
-      Node ns1 = NodeManager::currentNM()->mkConst(::CVC4::String(s1));
-      Node ns3 = NodeManager::currentNM()->mkConst(::CVC4::String(s3));
+      String s1 = s.substr(0, (int)p);
+      String s3 = s.substr((int)p + (int)t.size());
       std::vector<Node> children;
-      children.push_back(ns1);
+      if (s1.size() > 0)
+      {
+        Node ns1 = nm->mkConst(String(s1));
+        children.push_back(ns1);
+      }
       children.push_back(node[2]);
-      children.push_back(ns3);
+      if (s3.size() > 0)
+      {
+        Node ns3 = nm->mkConst(String(s3));
+        children.push_back(ns3);
+      }
       children.insert(children.end(), children0.begin() + 1, children0.end());
       Node ret = utils::mkConcat(STRING_CONCAT, children);
       return returnRewrite(node, ret, "rpl-const-find");
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 90641fe2f..0ac2d4142 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -853,6 +853,7 @@ set(regress_0_tests
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/re.all.smt2
   regress0/strings/repl-rewrites2.smt2
+  regress0/strings/replace-const.smt2
   regress0/strings/replaceall-eval.smt2
   regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2
diff --git a/test/regress/regress0/strings/replace-const.smt2 b/test/regress/regress0/strings/replace-const.smt2
new file mode 100644
index 000000000..a7f225e33
--- /dev/null
+++ b/test/regress/regress0/strings/replace-const.smt2
@@ -0,0 +1,12 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= x (str.replace "AA" "AA" "def")))
+(assert (= y (str.replace "BAA" "B" "def")))
+(assert (= z (str.replace "AAB" "B" "def")))
+
+(check-sat)
-- 
2.30.2