1 files changed, 12 insertions, 6 deletions
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 8e998b9cf..16d297495 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -16,21 +16,27 @@
 #include "smt/witness_form.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/env.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
 namespace smt {
 
-WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
-    : d_tcpg(pnm,
+WitnessFormGenerator::WitnessFormGenerator(Env& env)
+    : d_rewriter(env.getRewriter()),
+      d_tcpg(env.getProofNodeManager(),
              nullptr,
              TConvPolicy::FIXPOINT,
              TConvCachePolicy::NEVER,
              "WfGenerator::TConvProofGenerator",
              nullptr,
              true),
-      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"),
-      d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof")
+      d_wintroPf(env.getProofNodeManager(),
+                 nullptr,
+                 nullptr,
+                 "WfGenerator::LazyCDProof"),
+      d_pskPf(
+          env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof")
 {
 }
 
@@ -114,12 +120,12 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
 
 bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const
 {
-  return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s);
+  return d_rewriter->rewrite(t) != d_rewriter->rewrite(s);
 }
 
 bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const
 {
-  Node tr = theory::Rewriter::rewrite(t);
+  Node tr = d_rewriter->rewrite(t);
   return !tr.isConst() || !tr.getConst<bool>();
 }