This commit fixes a bug related to a public header depending on a compiler flag. This resulted in user code seeing a different size for the SmtEngine class than what was compiled in the library. Proofs are enabled by default again. See http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688 for more information.

1 files changed, 9 insertions, 8 deletions

diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 701775c9c..bc978b728 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -17,14 +17,15 @@
 
 #include "cvc4_private.h"
 
+#pragma once
+
+#include "expr/node_manager.h"
 #include "smt/smt_engine.h"
-#include "util/tls.h"
+#include "smt/options.h"
+#include "util/configuration_private.h"
 #include "util/cvc4_assert.h"
-#include "expr/node_manager.h"
 #include "util/output.h"
-#include "proof/proof.h"
-
-#pragma once
+#include "util/tls.h"
 
 namespace CVC4 {
 
@@ -43,14 +44,14 @@ inline bool smtEngineInScope() {
 }
 
 inline ProofManager* currentProofManager() {
-#ifdef CVC4_PROOF
+#if IS_PROOFS_BUILD
   Assert(options::proof() || options::unsatCores());
   Assert(s_smtEngine_current != NULL);
   return s_smtEngine_current->d_proofManager;
-#else /* CVC4_PROOF */
+#else /* IS_PROOFS_BUILD */
   InternalError("proofs/unsat cores are not on, but ProofManager requested");
   return NULL;
-#endif /* CVC4_PROOF */
+#endif /* IS_PROOFS_BUILD */
 }
 
 class SmtScope : public NodeManagerScope {