Moved the assertion to a better spot

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 43328e1de05b9fdbedcb792e029e9ddcce451669..9b3d9a289019926a1fb737e5329c7b7f96b702e2 100644 (file)
--- 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;