Minor

3 files changed, 38 insertions, 18 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 349a8b4fb..6ec1f28c6 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2285,13 +2285,16 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
         // past the first position in node[0] that contains node[1], we can drop
         std::vector<Node> nb;
         std::vector<Node> ne;
-        int cc = componentContains(children0, children1, nb, ne, true, 1);
-        if (cc != -1 && !ne.empty())
+        int cc = componentContains(children0, children1, nb, ne, true, 0);
+        if (cc != -1 && (!nb.empty() || !ne.empty()))
         {
           // For example:
           // str.indexof(str.++(x,y,z),y,0) ---> str.indexof(str.++(x,y),y,0)
           Node nn = mkConcat(kind::STRING_CONCAT, children0);
-          Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
+          Node ret = nm->mkNode(
+              PLUS,
+              nm->mkNode(STRING_LENGTH, mkConcat(STRING_CONCAT, nb)),
+              nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]));
           return returnRewrite(node, ret, "idof-def-ctn");
         }
       }
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 8b0072f52..81bc29ad6 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -472,7 +472,7 @@ class TheoryStringsRewriter {
    * @return true node if it can be shown that `a` contains `b`, false node if
    * it can be shown that `a` does not contain `b`, null node otherwise
    */
-  static Node checkEntailContains(Node a, Node b, bool fullRewriter = false);
+  static Node checkEntailContains(Node a, Node b, bool fullRewriter = true);
 
   /** entail non-empty
    *
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 760e35471..457e78cfc 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -500,19 +500,33 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
       sameNormalForm(idof, negOne);
     }
 
-    // (str.indexof (str.++ (str.substr (str.substr x 0 (str.indexof "A" 0)) 0
-    // 1) "B") 0) ---> -1
+    Node substr_substr_idof =
+        d_nm->mkNode(kind::STRING_SUBSTR, substr_idof, zero, one);
+
+    // (str.indexof (str.++
+    //   (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1) "B") 0) --->
+    // -1
     {
-      Node idof = d_nm->mkNode(
-          kind::STRING_STRIDOF,
-          d_nm->mkNode(
-              kind::STRING_CONCAT,
-              d_nm->mkNode(kind::STRING_SUBSTR, substr_idof, zero, one),
-              b),
-          a,
-          zero);
+      Node idof =
+          d_nm->mkNode(kind::STRING_STRIDOF,
+                       d_nm->mkNode(kind::STRING_CONCAT, substr_substr_idof, b),
+                       a,
+                       zero);
       sameNormalForm(idof, negOne);
     }
+
+    // (str.indexof (str.++
+    //   (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1) "A") 0) --->
+    // (str.len (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1))
+    {
+      Node lhs =
+          d_nm->mkNode(kind::STRING_STRIDOF,
+                       d_nm->mkNode(kind::STRING_CONCAT, substr_substr_idof, a),
+                       a,
+                       zero);
+      Node rhs = d_nm->mkNode(kind::STRING_LENGTH, substr_substr_idof);
+      sameNormalForm(lhs, rhs);
+    }
   }
 
   void testRewriteReplace()
@@ -918,8 +932,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     }
 
     {
-      // (str.contains (str.substr (str.substr x 0 (str.indexof x "AAC" zero)) 0
-      // n) "B") ---> false
+      // (str.contains
+      //   (str.substr
+      //     (str.substr x 0 (str.indexof x "AAC" zero)) 0 n) "B") --->
+      // false
       Node ctn = d_nm->mkNode(
           kind::STRING_STRCTN,
           d_nm->mkNode(kind::STRING_SUBSTR,
@@ -931,8 +947,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     }
 
     {
-      // (str.contains (str.substr (str.substr x 0 (str.indexof x "A" zero)) 0
-      // 1) "A") ---> false
+      // (str.contains
+      //   (str.substr (str.substr x 0 (str.indexof x "A" zero)) 0 1) "A") --->
+      // false
       Node ctn = d_nm->mkNode(
           kind::STRING_STRCTN,
           d_nm->mkNode(