1 files changed, 14 insertions, 10 deletions

diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp
index a1f56eaba..c2c6cf77e 100644
--- a/test/unit/theory/evaluator_white.cpp
+++ b/test/unit/theory/evaluator_white.cpp
@@ -59,10 +59,11 @@ TEST_F(TestTheoryWhiteEvaluator, simple)
   std::vector<Node> args = {w, x, y, z};
   std::vector<Node> vals = {c1, zero, one, c1};
 
-  Evaluator eval;
+  Rewriter* rr = d_smtEngine->getRewriter();
+  Evaluator eval(rr);
   Node r = eval.eval(t, args, vals);
   ASSERT_EQ(r,
-            Rewriter::rewrite(t.substitute(
+            rr->rewrite(t.substitute(
                 args.begin(), args.end(), vals.begin(), vals.end())));
 }
 
@@ -90,10 +91,11 @@ TEST_F(TestTheoryWhiteEvaluator, loop)
 
   std::vector<Node> args = {x};
   std::vector<Node> vals = {c};
-  Evaluator eval;
+  Rewriter* rr = d_smtEngine->getRewriter();
+  Evaluator eval(rr);
   Node r = eval.eval(t, args, vals);
   ASSERT_EQ(r,
-            Rewriter::rewrite(t.substitute(
+            rr->rewrite(t.substitute(
                 args.begin(), args.end(), vals.begin(), vals.end())));
 }
 
@@ -106,30 +108,31 @@ TEST_F(TestTheoryWhiteEvaluator, strIdOf)
 
   std::vector<Node> args;
   std::vector<Node> vals;
-  Evaluator eval;
+  Rewriter* rr = d_smtEngine->getRewriter();
+  Evaluator eval(rr);
 
   {
     Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, one);
     Node r = eval.eval(n, args, vals);
-    ASSERT_EQ(r, Rewriter::rewrite(n));
+    ASSERT_EQ(r, rr->rewrite(n));
   }
 
   {
     Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, one);
     Node r = eval.eval(n, args, vals);
-    ASSERT_EQ(r, Rewriter::rewrite(n));
+    ASSERT_EQ(r, rr->rewrite(n));
   }
 
   {
     Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, two);
     Node r = eval.eval(n, args, vals);
-    ASSERT_EQ(r, Rewriter::rewrite(n));
+    ASSERT_EQ(r, rr->rewrite(n));
   }
 
   {
     Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, two);
     Node r = eval.eval(n, args, vals);
-    ASSERT_EQ(r, Rewriter::rewrite(n));
+    ASSERT_EQ(r, rr->rewrite(n));
   }
 }
 
@@ -140,7 +143,8 @@ TEST_F(TestTheoryWhiteEvaluator, code)
 
   std::vector<Node> args;
   std::vector<Node> vals;
-  Evaluator eval;
+  Rewriter* rr = d_smtEngine->getRewriter();
+  Evaluator eval(rr);
 
   // (str.code "A") ---> 65
   {