Moved the assertion to a better spot

1 files changed, 2 insertions, 1 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 43328e1de..9b3d9a289 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -69,7 +69,6 @@ ProofManager::~ProofManager() {
 }
 
 ProofManager* ProofManager::currentPM() {
-  Assert(PROOF_ON(), "Cannot call ProofManager when proofs are off");
   return smt::currentProofManager();
 }
 
@@ -294,6 +293,8 @@ void ProofManager::traceUnsatCore() {
 }
 
 void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) {
+  Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
+
   d_satProof->constructProof();
 
   IdToSatClause used_lemmas;