Fix issue with str.idof in evaluator

The evaluator was evaluating `(str.idof "A" "" 1)` to `-1` instead of
`1` due to a wrong bound check. This commit fixes the issue.

2 files changed, 38 insertions, 1 deletions

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 4285a65cf..25e20451a 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -355,7 +355,7 @@ EvalResult Evaluator::evalInternal(TNode n,
           const String& x = results[currNode[1]].d_str;
           Integer i = results[currNode[2]].d_rat.getNumerator();
 
-          if (i.strictlyNegative() || i >= s_len)
+          if (i.strictlyNegative())
           {
             results[currNode] = EvalResult(Rational(-1));
           }
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 10cb15f6f..73556c388 100644
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -26,6 +26,7 @@
 #include "theory/evaluator.h"
 #include "theory/rewriter.h"
 #include "theory/theory_test_utils.h"
+#include "util/rational.h"
 
 using namespace CVC4;
 using namespace CVC4::smt;
@@ -119,4 +120,40 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
                      Rewriter::rewrite(t.substitute(
                          args.begin(), args.end(), vals.begin(), vals.end())));
   }
+
+  void testStrIdOf()
+  {
+    Node a = d_nm->mkConst(String("A"));
+    Node empty = d_nm->mkConst(String(""));
+    Node one = d_nm->mkConst(Rational(1));
+    Node two = d_nm->mkConst(Rational(2));
+
+    std::vector<Node> args;
+    std::vector<Node> vals;
+    Evaluator eval;
+
+    {
+      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, one);
+      Node r = eval.eval(n, args, vals);
+      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+    }
+
+    {
+      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, one);
+      Node r = eval.eval(n, args, vals);
+      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+    }
+
+    {
+      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, empty, two);
+      Node r = eval.eval(n, args, vals);
+      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+    }
+
+    {
+      Node n = d_nm->mkNode(kind::STRING_STRIDOF, a, a, two);
+      Node r = eval.eval(n, args, vals);
+      TS_ASSERT_EQUALS(r, Rewriter::rewrite(n));
+    }
+  }
 };