Fix issue with str.idof in evaluator (#2493)

1 files changed, 37 insertions, 0 deletions

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));
+    }
+  }
 };