From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 2 Nov 2011 13:05:11 +0000 (+0000)
Subject: give an option error if the user specifies --proof in a non-proof-enabled build
X-Git-Tag: cvc5-1.0.0~8390
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d183c7e68eb5b191fcc9d52eaeb86ce1211ba9f7;p=cvc5.git

give an option error if the user specifies --proof in a non-proof-enabled build
---

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: