diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
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; |