From: Gereon Kremer <nafur42@gmail.com>
Date: Tue, 8 Jun 2021 15:21:45 +0000 (+0200)
Subject: Fix statistics option handler (#6703)
X-Git-Tag: cvc5-1.0.0~1628
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b7e493bb78c86876e51e2e706bdeb4d33958798;p=cvc5.git

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 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