summaryrefslogtreecommitdiff
path: root/src/util/configuration_private.h
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2011-10-28 19:24:38 +0000
committerLiana Hadarean <lianahady@gmail.com>2011-10-28 19:24:38 +0000
commitb084a7efa9d65ec2f7475caa8486f8fd4cbafbd5 (patch)
treee118097c88787b7f2899bb8b2cbf865d058ef6bf /src/util/configuration_private.h
parent9547a48a7cdab8786c080779930de9c39655c52b (diff)
merged the proofgen3 branch into trunk:
- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.
Diffstat (limited to 'src/util/configuration_private.h')
-rw-r--r--src/util/configuration_private.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index abff15b3b..53b69ebfc 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -67,6 +67,12 @@ namespace CVC4 {
# define IS_ASSERTIONS_BUILD false
#endif /* CVC4_ASSERTIONS */
+#ifdef CVC4_PROOF
+# define IS_PROOFS_BUILD true
+#else /* CVC4_PROOF */
+# define IS_PROOFS_BUILD false
+#endif /* CVC4_PROOF */
+
#ifdef CVC4_COVERAGE
# define IS_COVERAGE_BUILD true
#else /* CVC4_COVERAGE */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback