summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-04-16 17:12:03 +0200
committerGitHub <noreply@github.com>2021-04-16 15:12:03 +0000
commit353006984c0c7bbd1bd419c04e4bb873c7eee52a (patch)
treed82c08a7f2cc8c4bd6ea5899ebb1829124a36503
parent6203bcb456d5450770c8ac6cdb775ec0f73e0325 (diff)
Fix dependencies for stats options (#6378)
A last-minute edit in a previous PR broke the handling of dependencies between the statistic options.
-rw-r--r--src/options/options_handler.cpp10
1 files changed, 6 insertions, 4 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 35a9673e2..3c5616c73 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -275,24 +275,26 @@ 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);
if (value)
{
- if (option == options::statisticsAll.getName())
+ if (opt == options::statisticsAll.getName())
{
d_options->d_holder->statistics = true;
}
- else if (option == options::statisticsEveryQuery.getName())
+ else if (opt == options::statisticsEveryQuery.getName())
{
d_options->d_holder->statistics = true;
}
- else if (option == options::statisticsExpert.getName())
+ else if (opt == options::statisticsExpert.getName())
{
d_options->d_holder->statistics = true;
}
}
else
{
- if (option == options::statistics.getName())
+ if (opt == options::statistics.getName())
{
d_options->d_holder->statisticsAll = false;
d_options->d_holder->statisticsEveryQuery = false;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback