diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp
index 435a767e4cd..17724d15645 100644
--- a/src/proof/alf/alf_printer.cpp
+++ b/src/proof/alf/alf_printer.cpp
@@ -635,6 +635,7 @@ void AlfPrinter::print(AlfPrintChannelOut& aout,
       dscope != nullptr ? dscope->getArguments() : d_emptyVec;
   const std::vector<Node>& assertions =
       ascope != nullptr ? ascope->getArguments() : d_emptyVec;
+
   bool wasAlloc;
   for (size_t i = 0; i < 2; i++)
   {
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index baf2af9a1ee..4a9127c1f3d 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -28,6 +28,7 @@
 #include "options/strings_options.h"
 #include "printer/printer.h"
 #include "proof/conv_proof_generator.h"
+#include "smt/proof_manager.h"
 #include "smt/solver_engine_stats.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/oracle_checker.h"
@@ -45,6 +46,7 @@ Env::Env(NodeManager* nm, const Options* opts)
     : d_nm(nm),
       d_context(new context::Context()),
       d_userContext(new context::UserContext()),
+      d_pfManager(nullptr),
       d_proofNodeManager(nullptr),
       d_rewriter(new theory::Rewriter(nm)),
       d_evalRew(nullptr),
@@ -76,12 +78,13 @@ Env::~Env() {}
 
 NodeManager* Env::getNodeManager() { return d_nm; }
 
-void Env::finishInit(ProofNodeManager* pnm)
+void Env::finishInit(smt::PfManager* pm)
 {
-  if (pnm != nullptr)
+  if (pm != nullptr)
   {
+    d_pfManager = pm;
     Assert(d_proofNodeManager == nullptr);
-    d_proofNodeManager = pnm;
+    d_proofNodeManager = pm->getProofNodeManager();
     d_rewriter->finishInit(*this);
   }
   d_topLevelSubs.reset(
@@ -104,6 +107,8 @@ context::Context* Env::getContext() { return d_context.get(); }
 
 context::UserContext* Env::getUserContext() { return d_userContext.get(); }
 
+smt::PfManager* Env::getProofManager() { return d_pfManager; }
+
 ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
 
 bool Env::isSatProofProducing() const
diff --git a/src/smt/env.h b/src/smt/env.h
index 270099e2b57..82ab8ad5748 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -88,7 +88,12 @@ class Env
 
   /** Get a pointer to the UserContext owned by this Env. */
   context::UserContext* getUserContext();
-
+  /**
+   * Get the underlying proof manager. Note since proofs depend on option
+   * initialization, this is only available after the SolverEngine that owns
+   * this environment is initialized, and only non-null if proofs are enabled.
+   */
+  smt::PfManager* getProofManager();
   /**
    * Get the underlying proof node manager. Note since proofs depend on option
    * initialization, this is only available after the SolverEngine that owns
@@ -317,7 +322,7 @@ class Env
   /* Private initialization ------------------------------------------------- */
 
   /** Set proof node manager if it exists */
-  void finishInit(ProofNodeManager* pnm);
+  void finishInit(smt::PfManager* pm);
 
   /* Private shutdown ------------------------------------------------------- */
   /**
@@ -333,6 +338,10 @@ class Env
   std::unique_ptr<context::Context> d_context;
   /** User level context owned by this Env */
   std::unique_ptr<context::UserContext> d_userContext;
+  /**
+   * The proof manager of the solver engine.
+   */
+  smt::PfManager* d_pfManager;
   /**
    * A pointer to the proof node manager, which is non-null if proofs are
    * enabled. This is owned by the proof manager of the SolverEngine that owns
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 4a402b5f2d5..cfbbee3bb7f 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -46,14 +46,15 @@ Preprocessor::Preprocessor(Env& env,
 
 Preprocessor::~Preprocessor() {}
 
-void Preprocessor::finishInit(TheoryEngine* te, prop::PropEngine* pe)
+void Preprocessor::finishInit(TheoryEngine* te,
+                              prop::PropEngine* pe,
+                              PreprocessProofGenerator* pppg)
 {
   // set up the preprocess proof generator, if necessary
-  if (options().smt.produceProofs && d_pppg == nullptr)
+  if (d_pppg == nullptr && pppg != nullptr)
   {
-    d_pppg = std::make_unique<PreprocessProofGenerator>(
-        d_env, userContext(), "smt::PreprocessProofGenerator");
-    d_propagator.enableProofs(userContext(), d_pppg.get());
+    d_pppg = pppg;
+    d_propagator.enableProofs(userContext(), d_pppg);
   }
 
   d_ppContext.reset(new preprocessing::PreprocessingPassContext(
@@ -129,7 +130,7 @@ void Preprocessor::applySubstitutions(std::vector<Node>& ns)
 
 PreprocessProofGenerator* Preprocessor::getPreprocessProofGenerator()
 {
-  return d_pppg.get();
+  return d_pppg;
 }
 
 }  // namespace smt
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index e9c81b7bb72..b902655f9aa 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -57,7 +57,9 @@ class Preprocessor : protected EnvObj
   /**
    * Finish initialization
    */
-  void finishInit(TheoryEngine* te, prop::PropEngine* pe);
+  void finishInit(TheoryEngine* te,
+                  prop::PropEngine* pe,
+                  PreprocessProofGenerator* pppg);
   /**
    * Process the assertions that have been asserted in argument as. Returns
    * true if no conflict was discovered while preprocessing them.
@@ -91,8 +93,8 @@ class Preprocessor : protected EnvObj
   PreprocessProofGenerator* getPreprocessProofGenerator();
 
  private:
-  /** The preprocess proof generator. */
-  std::unique_ptr<PreprocessProofGenerator> d_pppg;
+  /** Pointer to the preprocess proof generator. */
+  PreprocessProofGenerator* d_pppg;
   /**
    * A circuit propagator for non-clausal propositional deduction.
    */
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 382aac1393c..7878ae52f33 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -45,7 +45,8 @@ PfManager::PfManager(Env& env)
       d_rewriteDb(nullptr),
       d_pchecker(nullptr),
       d_pnm(nullptr),
-      d_pfpp(nullptr)
+      d_pfpp(nullptr),
+      d_pppg(nullptr)
 {
   // construct the rewrite db only if DSL rewrites are enabled
   if (options().proof.proofGranularityMode
@@ -75,6 +76,7 @@ PfManager::PfManager(Env& env)
       output(OutputTag::RARE_DB) << ss.str();
     }
   }
+
   // enable the proof checker and the proof node manager
   d_pchecker.reset(
       new ProofChecker(statisticsRegistry(),
@@ -140,6 +142,9 @@ PfManager::PfManager(Env& env)
     d_pfpp->setEliminateRule(ProofRule::TRUST);
   }
   d_false = nodeManager()->mkConst(false);
+
+  d_pppg = std::make_unique<PreprocessProofGenerator>(
+      d_env, userContext(), "smt::PreprocessProofGenerator");
 }
 
 PfManager::~PfManager() {}
@@ -157,11 +162,8 @@ constexpr typename std::vector<T, Alloc>::size_type erase_if(
 }
 
 std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
-    std::shared_ptr<ProofNode> pfn, SmtSolver& smt, ProofScopeMode scopeMode)
+    std::shared_ptr<ProofNode> pfn, Assertions& as, ProofScopeMode scopeMode)
 {
-  Assertions& as = smt.getAssertions();
-  PreprocessProofGenerator* pppg =
-      smt.getPreprocessor()->getPreprocessProofGenerator();
   // Note this assumes that connectProofToAssertions is only called once per
   // unsat response. This method would need to cache its result otherwise.
   Trace("smt-proof")
@@ -210,7 +212,7 @@ std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
   {
     d_pfpp->setAssertions(assertions, false);
   }
-  d_pfpp->process(pfn, pppg);
+  d_pfpp->process(pfn, d_pppg.get());
 
   switch (scopeMode)
   {
@@ -268,9 +270,10 @@ std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
 void PfManager::printProof(std::ostream& out,
                            std::shared_ptr<ProofNode> fp,
                            options::ProofFormatMode mode,
+                           ProofScopeMode scopeMode,
                            const std::map<Node, std::string>& assertionNames)
 {
-  Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
+  Trace("smt-proof") << "PfManager::printProof: start " << mode << std::endl;
   // We don't want to invalidate the proof nodes in fp, since these may be
   // reused in further check-sat calls, or they may be used again if the
   // user asks for the proof again (in non-incremental mode). We don't need to
@@ -290,10 +293,9 @@ void PfManager::printProof(std::ostream& out,
   }
   else if (mode == options::ProofFormatMode::CPC)
   {
-    Assert(fp->getRule() == ProofRule::SCOPE);
     proof::AlfNodeConverter atp(nodeManager());
     proof::AlfPrinter alfp(d_env, atp, d_rewriteDb.get());
-    alfp.print(out, fp);
+    alfp.print(out, fp, scopeMode);
   }
   else if (mode == options::ProofFormatMode::ALETHE)
   {
@@ -332,7 +334,7 @@ void PfManager::printProof(std::ostream& out,
 }
 
 void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
-                                       SmtSolver& smt)
+                                       Assertions& as)
 {
   Trace("difficulty-proc") << "Translate difficulty start" << std::endl;
   Trace("difficulty") << "PfManager::translateDifficultyMap" << std::endl;
@@ -361,7 +363,7 @@ void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
   cdp.addStep(fnode, ProofRule::SAT_REFUTATION, ppAsserts, {});
   std::shared_ptr<ProofNode> pf = cdp.getProofFor(fnode);
   Trace("difficulty-proc") << "Get final proof" << std::endl;
-  std::shared_ptr<ProofNode> fpf = connectProofToAssertions(pf, smt);
+  std::shared_ptr<ProofNode> fpf = connectProofToAssertions(pf, as);
   Trace("difficulty-debug") << "Final proof is " << *fpf.get() << std::endl;
   // We are typically a SCOPE here, although if we are not, then the proofs
   // have no free assumptions. If this is the case, then the only difficulty
@@ -408,6 +410,11 @@ rewriter::RewriteDb* PfManager::getRewriteDatabase() const
   return d_rewriteDb.get();
 }
 
+PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
+{
+  return d_pppg.get();
+}
+
 void PfManager::getAssertions(Assertions& as, std::vector<Node>& assertions)
 {
   // note that the assertion list is always available
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 82dcac5b1e4..4db96d2d3af 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -48,7 +48,6 @@ enum class ProofScopeMode
 namespace smt {
 
 class Assertions;
-class SmtSolver;
 class PreprocessProofGenerator;
 class ProofPostprocess;
 
@@ -92,10 +91,17 @@ class PfManager : protected EnvObj
   ~PfManager();
   /**
    * Print the proof on the given output stream in the given format.
+   *
+   * @param out The output stream.
+   * @param fp The proof to print.
+   * @param mode The format (e.g. cpc, alethe) to print.
+   * @param scopeMode The expected form of fp (see ProofScopeMode).
+   * @param assertionNames The named assertions of the input.
    */
   void printProof(std::ostream& out,
                   std::shared_ptr<ProofNode> fp,
                   options::ProofFormatMode mode,
+                  ProofScopeMode scopeMode,
                   const std::map<Node, std::string>& assertionNames =
                       std::map<Node, std::string>());
 
@@ -115,7 +121,7 @@ class PfManager : protected EnvObj
    * @param smt The SMT solver that owns the assertions and the preprocess
    * proof generator.
    */
-  void translateDifficultyMap(std::map<Node, Node>& dmap, SmtSolver& smt);
+  void translateDifficultyMap(std::map<Node, Node>& dmap, Assertions& as);
 
   /**
    * Connect proof to assertions
@@ -128,10 +134,14 @@ class PfManager : protected EnvObj
    * respect to assertions in as. Note this includes equalities of the form
    * (= f (lambda (...) t)) which originate from define-fun commands for f.
    * These are considered assertions in the final proof.
+   *
+   * @param pfn The proof.
+   * @param as Reference to the assertions.
+   * @param scopeMode The expected form of fp (see ProofScopeMode).
    */
   std::shared_ptr<ProofNode> connectProofToAssertions(
       std::shared_ptr<ProofNode> pfn,
-      SmtSolver& smt,
+      Assertions& as,
       ProofScopeMode scopeMode = ProofScopeMode::UNIFIED);
   //--------------------------- access to utilities
   /** Get a pointer to the ProofChecker owned by this. */
@@ -140,6 +150,8 @@ class PfManager : protected EnvObj
   ProofNodeManager* getProofNodeManager() const;
   /** Get the rewrite database, containing definitions of rewrites from DSL. */
   rewriter::RewriteDb* getRewriteDatabase() const;
+  /** Get the preprocess proof generator */
+  PreprocessProofGenerator* getPreprocessProofGenerator() const;
   //--------------------------- end access to utilities
  private:
   /**
@@ -162,6 +174,8 @@ class PfManager : protected EnvObj
   std::unique_ptr<ProofNodeManager> d_pnm;
   /** The proof post-processor */
   std::unique_ptr<smt::ProofPostprocess> d_pfpp;
+  /** The preprocess proof generator. */
+  std::unique_ptr<PreprocessProofGenerator> d_pppg;
 }; /* class SolverEngine */
 
 }  // namespace smt
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index a065c9e1964..422404669e1 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -24,6 +24,7 @@
 #include "smt/env.h"
 #include "smt/logic_exception.h"
 #include "smt/preprocessor.h"
+#include "smt/proof_manager.h"
 #include "smt/solver_engine_stats.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
@@ -81,7 +82,7 @@ void SmtSolver::finishInit()
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
   d_propEngine->finishInit();
-  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
+  finishInitPreprocessor();
 }
 
 void SmtSolver::resetAssertions()
@@ -98,7 +99,7 @@ void SmtSolver::resetAssertions()
   // depend on knowing the associated PropEngine.
   d_propEngine->finishInit();
   // must reset the preprocessor as well
-  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
+  finishInitPreprocessor();
 }
 
 void SmtSolver::interrupt()
@@ -232,5 +233,17 @@ void SmtSolver::resetTrail()
   d_propEngine->resetTrail();
 }
 
+void SmtSolver::finishInitPreprocessor()
+{
+  // determine if we are assigning a preprocess proof generator here
+  smt::PfManager* pm = d_env.getProofManager();
+  smt::PreprocessProofGenerator* pppg = nullptr;
+  if (pm != nullptr)
+  {
+    pppg = pm->getPreprocessProofGenerator();
+  }
+  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get(), pppg);
+}
+
 }  // namespace smt
 }  // namespace cvc5::internal
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 058d316cd87..66b4be1ae1a 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -135,6 +135,8 @@ class SmtSolver : protected EnvObj
  private:
   /** Whether we track information necessary for deep restarts */
   bool trackPreprocessedAssertions() const;
+  /** Finish initialization of preprocessor */
+  void finishInitPreprocessor();
   /** The preprocessor of this SMT solver */
   Preprocessor d_pp;
   /** Assertions manager */
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 6723e504a8f..989077189a1 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -180,7 +180,6 @@ void SolverEngine::finishInit()
   SetDefaults sdefaults(*d_env, d_isInternalSubsolver);
   sdefaults.setDefaults(d_env->d_logic, getOptions());
 
-  ProofNodeManager* pnm = nullptr;
   if (d_env->getOptions().smt.produceProofs)
   {
     // ensure bound variable uses canonical bound variables
@@ -190,7 +189,6 @@ void SolverEngine::finishInit()
     // start the unsat core manager
     d_ucManager.reset(new UnsatCoreManager(
         *d_env.get(), *d_smtSolver.get(), *d_pfManager.get()));
-    pnm = d_pfManager->getProofNodeManager();
   }
   if (d_env->isOutputOn(OutputTag::RARE_DB))
   {
@@ -203,7 +201,7 @@ void SolverEngine::finishInit()
     }
   }
   // enable proof support in the environment/rewriter
-  d_env->finishInit(pnm);
+  d_env->finishInit(d_pfManager.get());
 
   Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
   d_smtSolver->finishInit();
@@ -1454,7 +1452,11 @@ void SolverEngine::printProof(std::ostream& out,
     case modes::ProofFormat::LFSC: mode = options::ProofFormatMode::LFSC; break;
   }
 
-  d_pfManager->printProof(out, fp, mode, assertionNames);
+  d_pfManager->printProof(out,
+                          fp,
+                          mode,
+                          ProofScopeMode::DEFINITIONS_AND_ASSERTIONS,
+                          assertionNames);
   out << std::endl;
 }
 
@@ -1538,7 +1540,7 @@ void SolverEngine::checkProof()
   {
     // connect proof to assertions, which will fail if the proof is malformed
     d_pfManager->connectProofToAssertions(
-        pePfn, *d_smtSolver.get(), ProofScopeMode::UNIFIED);
+        pePfn, d_smtSolver->getAssertions(), ProofScopeMode::UNIFIED);
   }
 }
 
@@ -1785,7 +1787,7 @@ std::vector<std::shared_ptr<ProofNode>> SolverEngine::getProof(
     {
       Assert(p != nullptr);
       p = d_pfManager->connectProofToAssertions(
-          p, *d_smtSolver.get(), scopeMode);
+          p, d_smtSolver->getAssertions(), scopeMode);
     }
   }
   return ps;
@@ -1796,7 +1798,8 @@ void SolverEngine::proofToString(std::ostream& out,
 {
   options::ProofFormatMode format_mode =
       getOptions().proof.proofFormatMode;
-  d_pfManager->printProof(out, fp, format_mode);
+  d_pfManager->printProof(
+      out, fp, format_mode, ProofScopeMode::DEFINITIONS_AND_ASSERTIONS);
 }
 
 void SolverEngine::printInstantiations(std::ostream& out)
@@ -2046,7 +2049,7 @@ void SolverEngine::getDifficultyMap(std::map<Node, Node>& dmap)
   // do not include lemmas
   te->getDifficultyMap(dmap, false);
   // then ask proof manager to translate dmap in terms of the input
-  d_pfManager->translateDifficultyMap(dmap, *d_smtSolver.get());
+  d_pfManager->translateDifficultyMap(dmap, d_smtSolver->getAssertions());
 }
 
 void SolverEngine::push()
diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp
index 5f3318d64d2..26521d46b54 100644
--- a/src/smt/unsat_core_manager.cpp
+++ b/src/smt/unsat_core_manager.cpp
@@ -309,8 +309,8 @@ std::vector<Node> UnsatCoreManager::convertPreprocessedToInput(
   cdp.addStep(fnode, ProofRule::SAT_REFUTATION, ppa, {});
   std::shared_ptr<ProofNode> pepf = cdp.getProofFor(fnode);
   Assert(pepf != nullptr);
-  std::shared_ptr<ProofNode> pfn =
-      d_pfm.connectProofToAssertions(pepf, d_slv, ProofScopeMode::UNIFIED);
+  std::shared_ptr<ProofNode> pfn = d_pfm.connectProofToAssertions(
+      pepf, d_slv.getAssertions(), ProofScopeMode::UNIFIED);
   getUnsatCoreInternal(pfn, core, isInternal);
   return core;
 }
diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp
index b40dd054ac4..d7757f0c8e2 100644
--- a/test/unit/theory/theory_arith_coverings_white.cpp
+++ b/test/unit/theory/theory_arith_coverings_white.cpp
@@ -388,7 +388,7 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1)
   opts.write_smt().produceProofs = true;
   Env env(d_nodeManager, &opts);
   smt::PfManager pfm(env);
-  env.finishInit(pfm.getProofNodeManager());
+  env.finishInit(&pfm);
   EXPECT_TRUE(env.isTheoryProofProducing());
   // register checkers that we need
   NodeManager * nm = env.getNodeManager();