From bcb536ef60cb24c19001c0efbde55ff3a37e114f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 19 May 2021 12:12:28 -0500
Subject: [PATCH] Fix positive contains indexof rewrites for empty string
 second argument (#6566)

Fixes #6560.
---
 src/theory/strings/sequences_rewriter.cpp     | 41 +++++++++++--------
 test/regress/CMakeLists.txt                   |  1 +
 .../strings/issue6560-indexof-reduction.smt2  |  7 ++++
 3 files changed, 32 insertions(+), 17 deletions(-)
 create mode 100644 test/regress/regress0/strings/issue6560-indexof-reduction.smt2

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index ff718c124..1577a5625 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -2452,23 +2452,30 @@ Node SequencesRewriter::rewriteIndexof(Node node)
           return returnRewrite(node, ret, Rewrite::IDOF_STRIP_CNST_ENDPTS);
         }
       }
-
-      // strip symbolic length
-      Node new_len = node[2];
-      std::vector<Node> nr;
-      if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len))
-      {
-        // For example:
-        // z>str.len( x1 ) and str.contains( x2, y )-->true
-        // implies
-        // str.indexof( str.++( x1, x2 ), y, z ) --->
-        // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
-        Node nn = utils::mkConcat(children0, stype);
-        Node ret =
-            nm->mkNode(kind::PLUS,
-                       nm->mkNode(kind::MINUS, node[2], new_len),
-                       nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len));
-        return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
+      // To show that the first argument definitely contains the second, the
+      // index must be a valid index in the first argument. This ensures that
+      // (str.indexof t "" n) is not rewritten to something other than -1 when n
+      // is beyond the length of t. This is not required for the above rewrites,
+      // which only apply when n=0.
+      if (ArithEntail::check(node[2]) && ArithEntail::check(len0, node[2]))
+      {
+        // strip symbolic length
+        Node new_len = node[2];
+        std::vector<Node> nr;
+        if (StringsEntail::stripSymbolicLength(children0, nr, 1, new_len))
+        {
+          // For example:
+          // z>=0 and z>str.len( x1 ) and str.contains( x2, y )-->true
+          // implies
+          // str.indexof( str.++( x1, x2 ), y, z ) --->
+          // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) )
+          Node nn = utils::mkConcat(children0, stype);
+          Node ret =
+              nm->mkNode(PLUS,
+                         nm->mkNode(MINUS, node[2], new_len),
+                         nm->mkNode(STRING_STRIDOF, nn, node[1], new_len));
+          return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
+        }
       }
     }
     else
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 84ed52991..21a9f04b8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1131,6 +1131,7 @@ set(regress_0_tests
   regress0/strings/issue6203-3-unfold-trivial-true.smt2
   regress0/strings/issue6510-seq-bool.smt2
   regress0/strings/issue6520.smt2
+  regress0/strings/issue6560-indexof-reduction.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
diff --git a/test/regress/regress0/strings/issue6560-indexof-reduction.smt2 b/test/regress/regress0/strings/issue6560-indexof-reduction.smt2
new file mode 100644
index 000000000..bdb9d2877
--- /dev/null
+++ b/test/regress/regress0/strings/issue6560-indexof-reduction.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () String)
+(assert (> (str.indexof a "" (* 2 (str.len a))) 0))
+(check-sat)
-- 
2.30.2