From 2dbe1f150d30f0fb0c8522f891104270ce09db4c Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Aug 2014 16:59:28 -0400
Subject: Unsat core infrastruture and API (SMT-LIB compliance to come).

---
 src/smt/smt_engine_scope.h | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src/smt/smt_engine_scope.h')

diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 54b9fa1d0..fb5810fd5 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -40,9 +40,14 @@ inline SmtEngine* currentSmtEngine() {
 }
 
 inline ProofManager* currentProofManager() {
-  Assert(PROOF_ON());
+#ifdef CVC4_PROOF
+  Assert(options::proof() || options::unsatCores());
   Assert(s_smtEngine_current != NULL);
   return s_smtEngine_current->d_proofManager;
+#else /* CVC4_PROOF */
+  InternalError("proofs/unsat cores are not on, but ProofManager requested");
+  return NULL;
+#endif /* CVC4_PROOF */
 }
 
 class SmtScope : public NodeManagerScope {
-- 
cgit v1.2.3