[proofs] Make sure --proof-check=... is no-op when not checking proofs (#7638)

Fixes cvc5/cvc5-projects#342

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index a10f3210f109fd2fc7185b8eedeb9168e69fc329..2cf4862a9d67b49e96c710f4876e2e49c0d1da76 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -799,20 +799,10 @@ Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate a proof correctly.
-    if (d_env->getOptions().smt.checkProofs
-        || d_env->getOptions().proof.proofCheck
-               == options::ProofCheckMode::EAGER)
+    if (d_env->getOptions().smt.checkProofs)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
-        if ((d_env->getOptions().smt.checkProofs
-             || d_env->getOptions().proof.proofCheck
-                    == options::ProofCheckMode::EAGER)
-            && !d_env->getOptions().smt.produceProofs)
-        {
-          throw ModalException(
-              "Cannot check-proofs because proofs were disabled.");
-        }
         checkProof();
       }
     }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bffb3e8cb55181f9a19d133944cc924df5d25b6d..4aae3899dc0e689a40bceff88b7332b766533952 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -872,6 +872,7 @@ set(regress_0_tests
   regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
   regress0/proofs/project-issue330-eqproof.smt2
   regress0/proofs/proj-issue326-nl-bounds-check.smt2
+  regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
   regress0/proofs/qgu-fuzz-3-chainres-checking.smt2

diff --git a/test/regress/regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2 b/test/regress/regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
new file mode 100644 (file)
index 0000000..8422570
--- /dev/null
+++ b/test/regress/regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :produce-unsat-cores true)
+(set-option :proof-check eager)
+(assert false)
+(check-sat)
\ No newline at end of file