summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-11-02 13:05:11 +0000
committerMorgan Deters <mdeters@gmail.com>2011-11-02 13:05:11 +0000
commitd183c7e68eb5b191fcc9d52eaeb86ce1211ba9f7 (patch)
treed6f32a141dd1767a4ae558c55475c74b756fa43a /src/util
parent161bf31cfa76271542790ec9a2c052e35d6bb1cb (diff)
give an option error if the user specifies --proof in a non-proof-enabled build
Diffstat (limited to 'src/util')
-rw-r--r--src/util/options.cpp4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 3e877c541..3b7b7b08c 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -638,7 +638,11 @@ throw(OptionException) {
break;
case PROOF:
+#ifdef CVC4_PROOF
proof = true;
+#else /* CVC4_PROOF */
+ throw OptionException("This is not a proof-enabled build of CVC4; --proof cannot be used");
+#endif /* CVC4_PROOF */
break;
case NO_TYPE_CHECKING:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback