Implement lazy proof checking modes (#7106)

[cvc5.git] / src / proof / proof_checker.cpp

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 1d5aa61b4fb19a47bb2a687bd4346b2cf5193bfe..28a09fc9c8f78a840fea304ca69b09c6a3392bc0 100644 (file)
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -85,8 +85,10 @@ ProofCheckerStatistics::ProofCheckerStatistics()
 {
 }
 
-ProofChecker::ProofChecker(uint32_t pclevel, rewriter::RewriteDb* rdb)
-    : d_pclevel(pclevel), d_rdb(rdb)
+ProofChecker::ProofChecker(bool eagerCheck,
+                           uint32_t pclevel,
+                           rewriter::RewriteDb* rdb)
+    : d_eagerCheck(eagerCheck), d_pclevel(pclevel), d_rdb(rdb)
 {
 }
 
@@ -245,7 +247,7 @@ Node ProofChecker::checkInternal(PfRule id,
     }
   }
   // fails if pedantic level is not met
-  if (options::proofEagerChecking())
+  if (d_eagerCheck)
   {
     std::stringstream serr;
     if (isPedanticFailure(id, serr, enableOutput))