Revert "Minor"

This reverts commit b6dcaeb9b1e430941f1f4345152ebad21634a0be.

1 files changed, 6 insertions, 10 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 8e69b6faf..f1cdcb9e9 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2061,17 +2061,13 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
   }
   else if (node[0].getKind() == kind::STRING_SUBSTR)
   {
-    if (checkEntailNonEmpty(node[1]))
+    Node zero = nm->mkConst(Rational(0));
+    if (node[0][1] == zero && node[0][2].getKind() == kind::STRING_STRIDOF
+        && node[0][0] == node[0][2][0] && node[0][2][1] == node[1]
+        && node[0][2][2] == zero && checkEntailNonEmpty(node[1]))
     {
-      Node lenNonCtn = nm->mkNode(
-          MINUS,
-          nm->mkNode(STRING_STRIDOF, node[0][0], node[1], node[0][1]),
-          node[0][1]);
-      if (checkEntailArith(lenNonCtn, node[0][2]))
-      {
-        Node ret = nm->mkConst(false);
-        return returnRewrite(node, ret, "ctn-substr-idof");
-      }
+      Node ret = nm->mkConst(false);
+      return returnRewrite(node, ret, "ctn-substr-idof");
     }
 
     Node substr = node[0];