1 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index d71b3635b..1309a05f9 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -18,10 +18,10 @@
 #include "expr/skolem_manager.h"
 #include "smt/env.h"
 #include "smt/term_formula_removal.h"
-#include "theory/evaluator.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory.h"
+#include "util/rational.h"
 
 using namespace cvc5::kind;
 
@@ -67,7 +67,7 @@ Node BuiltinProofRuleChecker::applySubstitutionRewrite(
     MethodId idr)
 {
   Node nks = applySubstitution(n, exp, ids, ida);
-  return d_env.getRewriter()->rewriteViaMethod(nks, idr);
+  return d_env.rewriteViaMethod(nks, idr);
 }
 
 bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp,
@@ -249,7 +249,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     {
       return Node::null();
     }
-    Node res = d_env.getRewriter()->rewriteViaMethod(args[0], idr);
+    Node res = d_env.rewriteViaMethod(args[0], idr);
     if (res.isNull())
     {
       return Node::null();
@@ -260,7 +260,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   {
     Assert(children.empty());
     Assert(args.size() == 1);
-    Node res = d_env.getRewriter()->rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
+    Node res = d_env.rewriteViaMethod(args[0], MethodId::RW_EVALUATE);
     if (res.isNull())
     {
       return Node::null();
@@ -302,7 +302,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
                              << SkolemManager::getOriginalForm(res) << std::endl;
     // **** NOTE: can rewrite the witness form here. This enables certain lemmas
     // to be provable, e.g. (= k t) where k is a purification Skolem for t.
-    res = Rewriter::rewrite(SkolemManager::getOriginalForm(res));
+    res = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res));
     if (!res.isConst() || !res.getConst<bool>())
     {
       Trace("builtin-pfcheck")
@@ -349,8 +349,8 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     if (res1 != res2)
     {
       // can rewrite the witness forms
-      res1 = Rewriter::rewrite(SkolemManager::getOriginalForm(res1));
-      res2 = Rewriter::rewrite(SkolemManager::getOriginalForm(res2));
+      res1 = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res1));
+      res2 = d_env.getRewriter()->rewrite(SkolemManager::getOriginalForm(res2));
       if (res1.isNull() || res1 != res2)
       {
         Trace("builtin-pfcheck") << "Failed to match results" << std::endl;