summaryrefslogtreecommitdiff
path: root/src/smt/proof_post_processor.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-02-22 16:07:16 -0600
committerGitHub <noreply@github.com>2021-02-22 16:07:16 -0600
commit71d72df0437607723256bbd7b4f28cd6c89fe40f (patch)
tree1021b9e166290db4637a0be447da359d0aed4752 /src/smt/proof_post_processor.cpp
parent580f3e93c2cc4564e6fa87d07426dc1ff87224e4 (diff)
(proof-new) Change proof-new option to proof (#5955)
Also moves several proof-specific options to proof_options.
Diffstat (limited to 'src/smt/proof_post_processor.cpp')
-rw-r--r--src/smt/proof_post_processor.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index ab8dd8f92..0898096f5 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -15,6 +15,7 @@
#include "smt/proof_post_processor.h"
#include "expr/skolem_manager.h"
+#include "options/proof_options.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "smt/smt_engine.h"
@@ -1110,7 +1111,7 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
{
PfRule r = pn->getRule();
// if not doing eager pedantic checking, fail if below threshold
- if (!options::proofNewEagerChecking())
+ if (!options::proofEagerChecking())
{
if (!d_pedanticFailure)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback