From 6e9aa79dc721158a0a6b0503f376727b7341ff5d Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 16 Nov 2021 14:51:25 -0300
Subject: [PATCH] [proofs] Make sure --proof-check=... is no-op when not
 checking proofs (#7638)

Fixes cvc5/cvc5-projects#342
---
 src/smt/solver_engine.cpp                            | 12 +-----------
 test/regress/CMakeLists.txt                          |  1 +
 ...oj-issue342-eager-checking-no-proof-checking.smt2 |  6 ++++++
 3 files changed, 8 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index a10f3210f..2cf4862a9 100644
--- 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 bffb3e8cb..4aae3899d 100644
--- 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
index 000000000..8422570ea
--- /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
-- 
2.30.2