summaryrefslogtreecommitdiff
path: root/src/smt/options_handlers.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/options_handlers.h')
-rw-r--r--src/smt/options_handlers.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index fc2b796d3..eeefd7af0 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -20,6 +20,7 @@
#define __CVC4__SMT__OPTIONS_HANDLERS_H
#include "cvc4autoconfig.h"
+#include "util/configuration_private.h"
#include "util/dump.h"
#include "util/resource_manager.h"
#include "smt/modal_exception.h"
@@ -307,13 +308,13 @@ inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt)
// ensure we are a proof-enabled build of CVC4
inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-#ifndef CVC4_PROOF
+#if !(IS_PROOFS_BUILD)
if(value) {
std::stringstream ss;
ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
throw OptionException(ss.str());
}
-#endif /* CVC4_PROOF */
+#endif /* IS_PROOFS_BUILD */
}
// This macro is used for setting :regular-output-channel and :diagnostic-output-channel
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback