5 files changed, 14 insertions, 9 deletions
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index 1eea6286b..1e322ccd3 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -256,7 +256,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; }
 
 void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
 {
-  if (options::proofEagerChecking())
+  if (options::proofCheck() == options::ProofCheckMode::EAGER)
   {
     // catch a pedantic failure now, which otherwise would not be
     // triggered since we are doing lazy proof generation
diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index ae35b346c..93b4cae19 100644
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -59,7 +59,7 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
 {
   PfRule r = pn->getRule();
   // if not doing eager pedantic checking, fail if below threshold
-  if (!options::proofEagerChecking())
+  if (options::proofCheck() != options::ProofCheckMode::EAGER)
   {
     if (!d_pedanticFailure)
     {
@@ -70,6 +70,10 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
       }
     }
   }
+  if (options::proofCheck() != options::ProofCheckMode::NONE)
+  {
+    d_pnm->ensureChecked(pn.get());
+  }
   uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
   if (plevel != 0)
   {
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 49f67e94c..ae5de49e9 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -33,7 +33,9 @@ namespace smt {
 
 PfManager::PfManager(Env& env, SmtEngine* smte)
     : d_env(env),
-      d_pchecker(new ProofChecker(options::proofPedantic())),
+      d_pchecker(new ProofChecker(
+          d_env.getOptions().proof.proofCheck == options::ProofCheckMode::EAGER,
+          d_env.getOptions().proof.proofPedantic)),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 3c9a82a61..65762a50b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -369,7 +369,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
                << reasonNoProofs.str() << "." << std::endl;
       opts.smt.produceProofs = false;
       opts.smt.checkProofs = false;
-      opts.proof.proofEagerChecking = false;
     }
   }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 27e7b8530..5403928ec 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -876,12 +876,14 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     }
     // Check that UNSAT results generate a proof correctly.
     if (d_env->getOptions().smt.checkProofs
-        || d_env->getOptions().proof.proofEagerChecking)
+        || d_env->getOptions().proof.proofCheck
+               == options::ProofCheckMode::EAGER)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
         if ((d_env->getOptions().smt.checkProofs
-             || d_env->getOptions().proof.proofEagerChecking)
+             || d_env->getOptions().proof.proofCheck
+                    == options::ProofCheckMode::EAGER)
             && !d_env->getOptions().smt.produceProofs)
         {
           throw ModalException(
@@ -1368,7 +1370,7 @@ void SmtEngine::checkProof()
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
-  if (d_env->getOptions().proof.proofEagerChecking)
+  if (d_env->getOptions().proof.proofCheck == options::ProofCheckMode::EAGER)
   {
     pe->checkProof(d_asserts->getAssertionList());
   }
@@ -1439,7 +1441,6 @@ std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
     // disable all proof options
     coreChecker->getOptions().smt.produceProofs = false;
     coreChecker->getOptions().smt.checkProofs = false;
-    coreChecker->getOptions().proof.proofEagerChecking = false;
 
     for (const Node& ucAssertion : core)
     {
@@ -1504,7 +1505,6 @@ void SmtEngine::checkUnsatCore() {
   // disable all proof options
   coreChecker->getOptions().smt.produceProofs = false;
   coreChecker->getOptions().smt.checkProofs = false;
-  coreChecker->getOptions().proof.proofEagerChecking = false;
 
   // set up separation logic heap if necessary
   TypeNode sepLocType, sepDataType;