Remove command-verbosity option (#7581)

This PR removes the command-verbosity option. It is implemented as a weird special case, and nobody seems to use it anyway.

7 files changed, 64 insertions, 184 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index be3652dd4..ae4dc1e9c 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -213,13 +213,6 @@ bool solverInvoke(api::Solver* solver,
   }
 
   cmd->invoke(solver, sm, out);
-  // ignore the error if the command-verbosity is 0 for this command
-  std::string commandName =
-      std::string("command-verbosity:") + cmd->getCommandName();
-  if (solver->getOption(commandName) == "0")
-  {
-    return true;
-  }
   return !cmd->fail();
 }
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 419167e7e..83f761428 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -208,9 +208,7 @@ void Command::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out)
   invoke(solver, sm);
   if (!(isMuted() && ok()))
   {
-    printResult(
-        out,
-        std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
+    printResult(out);
   }
 }
 
@@ -226,14 +224,11 @@ void CommandStatus::toStream(std::ostream& out, Language language) const
   Printer::getPrinter(language)->toStream(out, this);
 }
 
-void Command::printResult(std::ostream& out, uint32_t verbosity) const
+void Command::printResult(std::ostream& out) const
 {
-  if (d_commandStatus != NULL)
+  if (d_commandStatus != nullptr)
   {
-    if ((!ok() && verbosity >= 1) || verbosity >= 2)
-    {
-      out << *d_commandStatus;
-    }
+    out << *d_commandStatus;
   }
 }
 
@@ -320,9 +315,7 @@ void EchoCommand::invoke(api::Solver* solver,
   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
                            << std::endl;
   d_commandStatus = CommandSuccess::instance();
-  printResult(
-      out,
-      std::stoul(solver->getOption("command-verbosity:" + getCommandName())));
+  printResult(out);
 }
 
 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
@@ -460,11 +453,11 @@ void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm)
 
 api::Result CheckSatCommand::getResult() const { return d_result; }
 
-void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void CheckSatCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -531,12 +524,11 @@ api::Result CheckSatAssumingCommand::getResult() const
   return d_result;
 }
 
-void CheckSatAssumingCommand::printResult(std::ostream& out,
-                                          uint32_t verbosity) const
+void CheckSatAssumingCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -586,11 +578,11 @@ void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 api::Result QueryCommand::getResult() const { return d_result; }
-void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void QueryCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -895,11 +887,11 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 api::Result CheckSynthCommand::getResult() const { return d_result; }
-void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void CheckSynthCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -1514,11 +1506,11 @@ void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 api::Term SimplifyCommand::getResult() const { return d_result; }
-void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void SimplifyCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -1593,11 +1585,11 @@ void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 api::Term GetValueCommand::getResult() const { return d_result; }
-void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void GetValueCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -1671,12 +1663,11 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 api::Term GetAssignmentCommand::getResult() const { return d_result; }
-void GetAssignmentCommand::printResult(std::ostream& out,
-                                       uint32_t verbosity) const
+void GetAssignmentCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -1732,11 +1723,11 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void GetModelCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -1883,7 +1874,7 @@ void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void GetProofCommand::printResult(std::ostream& out) const
 {
   if (ok())
   {
@@ -1891,7 +1882,7 @@ void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
   }
   else
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
 }
 
@@ -1937,12 +1928,11 @@ void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetInstantiationsCommand::printResult(std::ostream& out,
-                                           uint32_t verbosity) const
+void GetInstantiationsCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2016,12 +2006,11 @@ void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetInterpolCommand::printResult(std::ostream& out,
-                                     uint32_t verbosity) const
+void GetInterpolCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2106,11 +2095,11 @@ void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void GetAbductCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2187,12 +2176,11 @@ api::Term GetQuantifierEliminationCommand::getResult() const
 {
   return d_result;
 }
-void GetQuantifierEliminationCommand::printResult(std::ostream& out,
-                                                  uint32_t verbosity) const
+void GetQuantifierEliminationCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2250,12 +2238,11 @@ std::vector<api::Term> GetUnsatAssumptionsCommand::getResult() const
   return d_result;
 }
 
-void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
-                                             uint32_t verbosity) const
+void GetUnsatAssumptionsCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2307,12 +2294,11 @@ void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetUnsatCoreCommand::printResult(std::ostream& out,
-                                      uint32_t verbosity) const
+void GetUnsatCoreCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2384,12 +2370,11 @@ void GetDifficultyCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-void GetDifficultyCommand::printResult(std::ostream& out,
-                                       uint32_t verbosity) const
+void GetDifficultyCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2464,12 +2449,11 @@ void GetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 std::string GetAssertionsCommand::getResult() const { return d_result; }
-void GetAssertionsCommand::printResult(std::ostream& out,
-                                       uint32_t verbosity) const
+void GetAssertionsCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else
   {
@@ -2618,11 +2602,11 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 std::string GetInfoCommand::getResult() const { return d_result; }
-void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void GetInfoCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else if (d_result != "")
   {
@@ -2719,11 +2703,11 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 }
 
 std::string GetOptionCommand::getResult() const { return d_result; }
-void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const
+void GetOptionCommand::printResult(std::ostream& out) const
 {
   if (!ok())
   {
-    this->Command::printResult(out, verbosity);
+    this->Command::printResult(out);
   }
   else if (d_result != "")
   {
diff --git a/src/smt/command.h b/src/smt/command.h
index 5733eb3e5..6ca5a7fc8 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -253,7 +253,7 @@ class CVC5_EXPORT Command
 
   /** Get the command status (it's NULL if we haven't run yet). */
   const CommandStatus* getCommandStatus() const { return d_commandStatus; }
-  virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const;
+  virtual void printResult(std::ostream& out) const;
 
   /**
    * Clone this Command (make a shallow copy).
@@ -595,7 +595,7 @@ class CVC5_EXPORT CheckSatCommand : public Command
   CheckSatCommand();
   api::Result getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -621,7 +621,7 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command
   const std::vector<api::Term>& getTerms() const;
   api::Result getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -646,7 +646,7 @@ class CVC5_EXPORT QueryCommand : public Command
   api::Term getTerm() const;
   api::Result getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -825,7 +825,7 @@ class CVC5_EXPORT CheckSynthCommand : public Command
   /** returns the result of the check-synth call */
   api::Result getResult() const;
   /** prints the result of the check-synth-call */
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   /** invokes this command
    *
    * This invocation makes the SMT engine build a synthesis conjecture based on
@@ -867,7 +867,7 @@ class CVC5_EXPORT SimplifyCommand : public Command
   api::Term getTerm() const;
   api::Term getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -889,7 +889,7 @@ class CVC5_EXPORT GetValueCommand : public Command
   const std::vector<api::Term>& getTerms() const;
   api::Term getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -908,7 +908,7 @@ class CVC5_EXPORT GetAssignmentCommand : public Command
 
   api::Term getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -922,7 +922,7 @@ class CVC5_EXPORT GetModelCommand : public Command
  public:
   GetModelCommand();
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -977,7 +977,7 @@ class CVC5_EXPORT GetProofCommand : public Command
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
 
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
 
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -998,7 +998,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command
 
   static bool isEnabled(api::Solver* solver, const api::Result& res);
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -1035,7 +1035,7 @@ class CVC5_EXPORT GetInterpolCommand : public Command
   api::Term getResult() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -1085,7 +1085,7 @@ class CVC5_EXPORT GetAbductCommand : public Command
   api::Term getResult() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -1121,7 +1121,7 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : public Command
   bool getDoFull() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   api::Term getResult() const;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
 
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1137,7 +1137,7 @@ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command
   GetUnsatAssumptionsCommand();
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   std::vector<api::Term> getResult() const;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -1156,7 +1156,7 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command
   const std::vector<api::Term>& getUnsatCore() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
 
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1179,7 +1179,7 @@ class CVC5_EXPORT GetDifficultyCommand : public Command
   const std::map<api::Term, api::Term>& getDifficultyMap() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
 
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1205,7 +1205,7 @@ class CVC5_EXPORT GetAssertionsCommand : public Command
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   std::string getResult() const;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -1266,7 +1266,7 @@ class CVC5_EXPORT GetInfoCommand : public Command
   std::string getResult() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
@@ -1309,7 +1309,7 @@ class CVC5_EXPORT GetOptionCommand : public Command
   std::string getResult() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  void printResult(std::ostream& out) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(std::ostream& out,
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 6dc40ac8b..a10f3210f 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1829,34 +1829,7 @@ void SolverEngine::printStatisticsDiff() const
 void SolverEngine::setOption(const std::string& key, const std::string& value)
 {
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
-
-  if (key == "command-verbosity")
-  {
-    size_t fstIndex = value.find(" ");
-    size_t sndIndex = value.find(" ", fstIndex + 1);
-    if (sndIndex == std::string::npos)
-    {
-      string c = value.substr(1, fstIndex - 1);
-      int v =
-          std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1));
-      if (v < 0 || v > 2)
-      {
-        throw OptionException("command-verbosity must be 0, 1, or 2");
-      }
-      d_commandVerbosity[c] = v;
-      return;
-    }
-    throw OptionException(
-        "command-verbosity value must be a tuple (command-name integer)");
-  }
-
-  if (value.find(" ") != std::string::npos)
-  {
-    throw OptionException("bad value for :" + key);
-  }
-
-  std::string optionarg = value;
-  options::set(getOptions(), key, optionarg);
+  options::set(getOptions(), key, value);
 }
 
 void SolverEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
@@ -1865,57 +1838,7 @@ bool SolverEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
 
 std::string SolverEngine::getOption(const std::string& key) const
 {
-  NodeManager* nm = d_env->getNodeManager();
-
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
-
-  if (key.find("command-verbosity:") == 0)
-  {
-    auto it =
-        d_commandVerbosity.find(key.substr(std::strlen("command-verbosity:")));
-    if (it != d_commandVerbosity.end())
-    {
-      return std::to_string(it->second);
-    }
-    it = d_commandVerbosity.find("*");
-    if (it != d_commandVerbosity.end())
-    {
-      return std::to_string(it->second);
-    }
-    return "2";
-  }
-
-  if (key == "command-verbosity")
-  {
-    vector<Node> result;
-    Node defaultVerbosity;
-    for (const auto& verb : d_commandVerbosity)
-    {
-      // treat the command name as a variable name as opposed to a string
-      // constant to avoid printing double quotes around the name
-      Node name = nm->mkBoundVar(verb.first, nm->integerType());
-      Node value = nm->mkConst(Rational(verb.second));
-      if (verb.first == "*")
-      {
-        // put the default at the end of the SExpr
-        defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value);
-      }
-      else
-      {
-        result.push_back(nm->mkNode(Kind::SEXPR, name, value));
-      }
-    }
-    // ensure the default is always listed
-    if (defaultVerbosity.isNull())
-    {
-      defaultVerbosity = nm->mkNode(Kind::SEXPR,
-                                    nm->mkBoundVar("*", nm->integerType()),
-                                    nm->mkConst(Rational(2)));
-    }
-    result.push_back(defaultVerbosity);
-    return nm->mkNode(Kind::SEXPR, result).toString();
-  }
-
   return options::get(getOptions(), key);
 }
 
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 7096aec92..d7df78f08 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -1086,11 +1086,6 @@ class CVC5_EXPORT SolverEngine
   /** Whether this is an internal subsolver. */
   bool d_isInternalSubsolver;
 
-  /**
-   * Verbosity of various commands.
-   */
-  std::map<std::string, int> d_commandVerbosity;
-
   /** The statistics class */
   std::unique_ptr<smt::SolverEngineStatistics> d_stats;
 
diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2
index 41012f888..edd3a2341 100644
--- a/test/regress/regress0/options/ast-and-sexpr.smt2
+++ b/test/regress/regress0/options/ast-and-sexpr.smt2
@@ -1,18 +1,9 @@
-; EXPECT: (SEXPR (SEXPR check-sat (CONST_RATIONAL 2)) (SEXPR * (CONST_RATIONAL 1)))
 ; EXPECT: (:status unknown)
 
 ; This regression tests uses of s-expressions when the output-language is AST
 
 (set-option :output-language ast)
 
-; Set the verbosity of all commands to 1
-(set-option :command-verbosity (* 1))
-; Set the verbosity of (check-sat) command to 2
-(set-option :command-verbosity (check-sat 2))
-; Get the verbosity of all commands
-(get-option :command-verbosity)
-; There is no SMT option to get the verbosity of a specific command
-
 (set-info :source (true false (- 15) 15 15.0 #b00001111 #x0f x |x 
 "| "" """"))
 (get-info :status)
diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2
index 24e05ec2a..afa779b05 100644
--- a/test/regress/regress0/options/set-and-get-options.smt2
+++ b/test/regress/regress0/options/set-and-get-options.smt2
@@ -1,14 +1,8 @@
-; EXPECT: ((* 2))
-; EXPECT: ((check-sat 1) (* 1))
 ; EXPECT: true
 ; EXPECT: false
 ; EXPECT: 15
 ; EXPECT: none
 
-(get-option :command-verbosity)
-(set-option :command-verbosity (* 1))
-(set-option :command-verbosity (check-sat 1))
-(get-option :command-verbosity)
 (set-option :check-models true)
 (get-option :check-models)
 (set-option :check-models false)