From d8c343c00426577ba94b3dc984557a9440b6b1bd Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 1 Aug 2020 02:20:24 -0500
Subject: [PATCH] Fix component contains for splicing due to substring. (#4705)

Fixes #4701. That benchmark now times out.
---
 src/theory/strings/strings_entail.cpp              | 14 ++++++++++++--
 test/regress/CMakeLists.txt                        |  1 +
 .../regress1/strings/issue4701_substr_splice.smt2  | 12 ++++++++++++
 3 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress1/strings/issue4701_substr_splice.smt2

diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 928414523..b2c2c3cd3 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -225,6 +225,9 @@ int StringsEntail::componentContains(std::vector<Node>& n1,
 {
   Assert(nb.empty());
   Assert(ne.empty());
+  Trace("strings-entail") << "Component contains: " << std::endl;
+  Trace("strings-entail") << "n1 = " << n1 << std::endl;
+  Trace("strings-entail") << "n2 = " << n2 << std::endl;
   // if n2 is a singleton, we can do optimized version here
   if (n2.size() == 1)
   {
@@ -301,6 +304,10 @@ int StringsEntail::componentContains(std::vector<Node>& n1,
                                       -1,
                                       computeRemainder && remainderDir != -1))
             {
+              Trace("strings-entail-debug")
+                  << "Last remainder begin is " << n1rb_last << std::endl;
+              Trace("strings-entail-debug")
+                  << "Last remainder end is " << n1re_last << std::endl;
               Assert(n1rb_last.isNull());
               if (computeRemainder)
               {
@@ -325,6 +332,9 @@ int StringsEntail::componentContains(std::vector<Node>& n1,
                   }
                 }
               }
+              Trace("strings-entail-debug") << "ne = " << ne << std::endl;
+              Trace("strings-entail-debug") << "nb = " << nb << std::endl;
+              Trace("strings-entail-debug") << "...return " << i << std::endl;
               return i;
             }
             else
@@ -444,12 +454,12 @@ bool StringsEntail::componentContainsBase(
               {
                 return false;
               }
-              if (dir != 1)
+              if (dir != -1)
               {
                 n1rb = nm->mkNode(
                     STRING_SUBSTR, n2[0], nm->mkConst(Rational(0)), start_pos);
               }
-              if (dir != -1)
+              if (dir != 1)
               {
                 n1re = nm->mkNode(STRING_SUBSTR, n2[0], end_pos, len_n2s);
               }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 95c272a3e..a0fee2185 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1808,6 +1808,7 @@ set(regress_1_tests
   regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
   regress1/strings/issue4379.smt2
   regress1/strings/issue4608-re-derive.smt2
+  regress1/strings/issue4701_substr_splice.smt2
   regress1/strings/issue4735.smt2
   regress1/strings/issue4735_2.smt2
   regress1/strings/issue4759-comp-delta.smt2
diff --git a/test/regress/regress1/strings/issue4701_substr_splice.smt2 b/test/regress/regress1/strings/issue4701_substr_splice.smt2
new file mode 100644
index 000000000..28e89588f
--- /dev/null
+++ b/test/regress/regress1/strings/issue4701_substr_splice.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_SLIA)
+(set-info :status sat)
+(set-option :strings-exp true)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(declare-fun e () String)
+(assert (= e (str.++ b (str.substr a 0 1))))
+(assert (= a (str.substr c 0 (str.len e))))
+(assert (= "a" b))
+(assert (= (str.++ b a) (str.replace c e a)))
+(check-sat)
-- 
2.30.2