2 files changed, 5 insertions, 6 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index a25903094..1be7b44c6 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -24,6 +24,7 @@
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory.h"
+#include "theory/quantifiers/extended_rewrite.h"
 
 using namespace cvc5::kind;
 
@@ -89,7 +90,8 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
   }
   if (idr == MethodId::RW_EXT_REWRITE)
   {
-    return d_ext_rewriter.extendedRewrite(n);
+    quantifiers::ExtendedRewriter er;
+    return er.extendedRewrite(n);
   }
   if (idr == MethodId::RW_REWRITE_EQ_EXT)
   {
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 2be44e586..0386978e6 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -22,7 +22,6 @@
 #include "proof/method_id.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node.h"
-#include "theory/quantifiers/extended_rewrite.h"
 
 namespace cvc5 {
 namespace theory {
@@ -43,7 +42,7 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * specifying a call to Rewriter::rewrite.
    * @return The rewritten form of n.
    */
-  Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
+  static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
   /**
    * Get substitution for literal exp. Updates vars/subs to the substitution
    * specified by exp for the substitution method ids.
@@ -100,7 +99,7 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * @param idr The method identifier of the rewriter.
    * @return The substituted, rewritten form of n.
    */
-  Node applySubstitutionRewrite(Node n,
+  static Node applySubstitutionRewrite(Node n,
                                 const std::vector<Node>& exp,
                                 MethodId ids = MethodId::SB_DEFAULT,
                                 MethodId ida = MethodId::SBA_SEQUENTIAL,
@@ -119,8 +118,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
                      const std::vector<Node>& children,
                      const std::vector<Node>& args) override;
 
-  /** extended rewriter object */
-  quantifiers::ExtendedRewriter d_ext_rewriter;
   /** Pointer to the rewrite database */
   rewriter::RewriteDb* d_rdb;
 };