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

diff --git a/src/options/base_options b/src/options/base_options
index 71754cca58e91bc97900545ca874500a11deafcc..f9eb64ef209608ab138c0b1848768337ab729fff 100644 (file)
--- 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 6b8d94c08c59e82bf25bf1062f9628bc2d4e95bc..dc4975ab5da5623809c9302dba618faaa7c49f0d 100644 (file)
--- 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 */