From c508e78395491bc5055e77169d39a97b5e6c8a5a Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Fri, 15 Jul 2016 16:53:54 -0700
Subject: [PATCH] Moved the assertion to a better spot

---
 src/proof/proof_manager.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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;
-- 
2.30.2