From: Guy <katz911@gmail.com>
Date: Fri, 15 Jul 2016 23:53:54 +0000 (-0700)
Subject: Moved the assertion to a better spot
X-Git-Tag: cvc5-1.0.0~6040^2~45
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c508e78395491bc5055e77169d39a97b5e6c8a5a;p=cvc5.git

Moved the assertion to a better spot
---

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;