Allow a caller to query whether an unsat core is available or not

1 files changed, 5 insertions, 0 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 9b3d9a289..09fc5dc8b 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -292,8 +292,13 @@ void ProofManager::traceUnsatCore() {
   }
 }
 
+bool ProofManager::unsatCoreAvailable() const {
+  return d_satProof->derivedEmptyClause();
+}
+
 void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) {
   Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
+  Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
 
   d_satProof->constructProof();