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, 25 insertions, 0 deletions

diff --git a/src/proof/proof.h b/src/proof/proof.h
index 440279dbc..25979dc46 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -21,6 +21,30 @@
 
 #include "smt/options.h"
 
+
+/* Do NOT use #ifdef CVC4_PROOF to check if proofs are enabled.
+ * We cannot assume users will use -DCVC4_PROOFS if they have a proofs build.
+ * The preferred way of checking that proofs are enabled is to use:
+ * #if IS_PROOFS_BUILD
+ * ...
+ * #endif
+ *
+ * The macro IS_PROOFS_BUILD is defined in util/configuration_private.h
+ *
+ * This has the effect of forcing that location to have included this header
+ * *before* performing this test. This includes C preprocessing expansion.
+ * This forces the inclusion of "cvc4_private.h". This is intentional!
+ *
+ * See bug 688 for more details:
+ * http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688
+ *
+ * If you want to check CVC4_PROOF, you should have a very good reason
+ * and should list the exceptions here:
+ * - Makefile.am
+ * - proof/proofs.h
+ * - util/configuration_private.h
+ */
+
 #ifdef CVC4_PROOF
 #  define PROOF(x) if(options::proof() || options::unsatCores()) { x; }
 #  define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL
@@ -31,4 +55,5 @@
 #  define PROOF_ON() false
 #endif /* CVC4_PROOF */
 
+
 #endif /* __CVC4__PROOF__PROOF_H */