Merge branch '1.4.x'

[cvc5.git] / src / smt / smt_engine_scope.h

diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 2389181b587dafb2767715d7ab037cdbdc226b61..fb5810fd54e9cfdf6b466041e61f4fc926492ee8 100644 (file)
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -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 {