From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 2 Apr 2013 19:51:44 +0000 (-0400)
Subject: Don't allow --stats if not a statistics-enabled build
X-Git-Tag: cvc5-1.0.0~7287^2~46
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3797216a84228b6685df1f2337e17b1a4de97722;p=cvc5.git

Don't allow --stats if not a statistics-enabled build
---

diff --git a/src/options/base_options b/src/options/base_options
index 71754cca5..f9eb64ef2 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -103,7 +103,7 @@ common-option - -v --verbose void :handler CVC4::options::increaseVerbosity
 common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity
  decrease verbosity (may be repeated)
 
-common-option statistics statistics --stats bool
+common-option statistics statistics --stats bool :predicate CVC4::smt::statsEnabledBuild :predicate-include "smt/options_handlers.h"
  give statistics on exit
 undocumented-alias --statistics = --stats
 undocumented-alias --no-statistics = --no-stats
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 6b8d94c08..dc4975ab5 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -409,6 +409,17 @@ inline std::ostream* checkReplayLogFilename(std::string option, std::string opta
 #endif /* CVC4_REPLAY */
 }
 
+// ensure we are a stats-enabled build of CVC4
+inline void statsEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
+#ifndef CVC4_STATISTICS_ON
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_STATISTICS_ON */
+}
+
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */