From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 16 Apr 2021 15:12:03 +0000 (+0200)
Subject: Fix dependencies for stats options (#6378)
X-Git-Tag: cvc5-1.0.0~1888
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=353006984c0c7bbd1bd419c04e4bb873c7eee52a;p=cvc5.git

Fix dependencies for stats options (#6378)

A last-minute edit in a previous PR broke the handling of dependencies between the statistic options.
---

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;