diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-02 15:51:44 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-24 16:50:04 -0400 |
commit | 3797216a84228b6685df1f2337e17b1a4de97722 (patch) | |
tree | adabde203c5a623c9b7c9652bd03525100cd3d2b /src | |
parent | 028b3ee2dce5ae7491f1019c32ac6faf6c4d6ef1 (diff) |
Don't allow --stats if not a statistics-enabled build
Diffstat (limited to 'src')
-rw-r--r-- | src/options/base_options | 2 | ||||
-rw-r--r-- | src/smt/options_handlers.h | 11 |
2 files changed, 12 insertions, 1 deletions
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 */ |