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.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d06c64517c70034aabcede8ca61b6664c39d6328..c1c843802bb6818ab28b1238f5fb0e06e1d59f75 100644 (file)
--- 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 d112bdf1d79edb5dec76e6f884ec0c845a625ba1..a5a687f9f5e5bc2b7e24221ef542d35196a24935 100644 (file)
--- 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 (file)
index 0000000..047c039
--- /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