summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGereon Kremer <nafur42@gmail.com>2021-06-08 17:21:45 +0200
committerGitHub <noreply@github.com>2021-06-08 15:21:45 +0000
commit6b7e493bb78c86876e51e2e706bdeb4d33958798 (patch)
tree681eec07063dff4b6fdcfd7a1980cf91e65b6a6a
parent52f02c087ca45a65c1e483faab32ac2078106aa0 (diff)
Fix statistics option handler (#6703)
This PR fixes a typo in the option handler for the statistics options, which lead to options not properly propagating.
-rw-r--r--src/options/options_handler.cpp15
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress0/options/statistics.smt242
3 files changed, 52 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;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d112bdf1d..a5a687f9f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -737,6 +737,7 @@ set(regress_0_tests
regress0/options/ast-and-sexpr.smt2
regress0/options/invalid_dump.smt2
regress0/options/set-and-get-options.smt2
+ regress0/options/statistics.smt2
regress0/parallel-let.smt2
regress0/parser/as.smt2
regress0/parser/bv_arity_smt2.6.smt2
diff --git a/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2
new file mode 100644
index 000000000..047c039ee
--- /dev/null
+++ b/test/regress/regress0/options/statistics.smt2
@@ -0,0 +1,42 @@
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+; EXPECT: true
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+(set-logic QF_UF)
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats-all true)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats false)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats-expert true)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert) \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback