diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/options/options_handler.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index d06c64517..c1c843802 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -252,26 +252,29 @@ void OptionsHandler::setStats(const std::string& option, bool value) throw OptionException(ss.str()); } #endif /* CVC5_STATISTICS_ON */ - Assert(option.substr(0, 2) == "--"); - std::string opt = option.substr(2); + std::string opt = option; + if (option.substr(0, 2) == "--") + { + opt = opt.substr(2); + } if (value) { - if (option == options::base::statisticsAll__name) + if (opt == options::base::statisticsAll__name) { d_options->base.statistics = true; } - else if (option == options::base::statisticsEveryQuery__name) + else if (opt == options::base::statisticsEveryQuery__name) { d_options->base.statistics = true; } - else if (option == options::base::statisticsExpert__name) + else if (opt == options::base::statisticsExpert__name) { d_options->base.statistics = true; } } else { - if (option == options::base::statistics__name) + if (opt == options::base::statistics__name) { d_options->base.statisticsAll = false; d_options->base.statisticsEveryQuery = false; |