From 0e03b178fb96f1bab934a8ccd064a3df44db42b3 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Mar 2022 13:48:28 -0500
Subject: [PATCH] Make IDOF_MAX rewrite only apply when all children are
 constant (#8363)

Fixes #8346.
---
 src/theory/strings/sequences_rewriter.cpp     | 44 +++++++++++--------
 test/regress/cli/CMakeLists.txt               |  1 +
 .../regress0/strings/issue8346-idof-max.smt2  |  8 ++++
 3 files changed, 34 insertions(+), 19 deletions(-)
 create mode 100644 test/regress/cli/regress0/strings/issue8346-idof-max.smt2

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 74b053cd2..ce95d193f 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -2549,27 +2549,33 @@ Node SequencesRewriter::rewriteIndexof(Node node)
     cvc5::Rational rMaxInt(cvc5::String::maxSize());
     if (node[2].getConst<Rational>() > rMaxInt)
     {
-      // We know that, due to limitations on the size of string constants
-      // in our implementation, that accessing a position greater than
-      // rMaxInt is guaranteed to be out of bounds.
-      Node negone = nm->mkConstInt(Rational(-1));
-      return returnRewrite(node, negone, Rewrite::IDOF_MAX);
-    }
-    Assert(node[2].getConst<Rational>().sgn() >= 0);
-    Node s = children0[0];
-    Node t = node[1];
-    uint32_t start =
-        node[2].getConst<Rational>().getNumerator().toUnsignedInt();
-    std::size_t ret = Word::find(s, t, start);
-    if (ret != std::string::npos)
-    {
-      Node retv = nm->mkConstInt(Rational(static_cast<unsigned>(ret)));
-      return returnRewrite(node, retv, Rewrite::IDOF_FIND);
+      if (node[0].isConst())
+      {
+        // We know that, due to limitations on the size of string constants
+        // in our implementation, that accessing a position greater than
+        // rMaxInt is guaranteed to be out of bounds.
+        Node negone = nm->mkConstInt(Rational(-1));
+        return returnRewrite(node, negone, Rewrite::IDOF_MAX);
+      }
     }
-    else if (children0.size() == 1)
+    else
     {
-      Node negone = nm->mkConstInt(Rational(-1));
-      return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
+      Assert(node[2].getConst<Rational>().sgn() >= 0);
+      Node s = children0[0];
+      Node t = node[1];
+      uint32_t start =
+          node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+      std::size_t ret = Word::find(s, t, start);
+      if (ret != std::string::npos)
+      {
+        Node retv = nm->mkConstInt(Rational(static_cast<unsigned>(ret)));
+        return returnRewrite(node, retv, Rewrite::IDOF_FIND);
+      }
+      else if (children0.size() == 1)
+      {
+        Node negone = nm->mkConstInt(Rational(-1));
+        return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
+      }
     }
   }
 
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index d263fe10d..67bcd6bca 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1370,6 +1370,7 @@ set(regress_0_tests
   regress0/strings/issue6834-str-eq-const-nhomog.smt2
   regress0/strings/issue7974-incomplete-neg-member.smt2
   regress0/strings/issue8295-star-union-char.smt2
+  regress0/strings/issue8346-idof-max.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
diff --git a/test/regress/cli/regress0/strings/issue8346-idof-max.smt2 b/test/regress/cli/regress0/strings/issue8346-idof-max.smt2
new file mode 100644
index 000000000..badb97e1a
--- /dev/null
+++ b/test/regress/cli/regress0/strings/issue8346-idof-max.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun str9 () String)
+(declare-fun i3 () Int)
+(assert (= 0 (- (str.indexof str9 (str.substr str9 1 1) i3) (- (* 137 (- (* 74 74 25 25 12)))))))
+(check-sat)
-- 
2.30.2