Start refactoring of `-o` and `-v` (#7449)

This PR does the first step in consolidating our various output mechanisms. The goal is to have only three major ways to output information:
- verbose(level) prints log-like information to the user via stderr, -v and -q increase and decrease the verbosity, respectively.
- output(tag) prints structured information (as s-expressions) to the user via stdout, -o enables individual tags.
- Trace(tag) prints log-like information to the developer via stdout, -t enables individual tags.
While Debug and Trace (and eventually Dump) will be combined within Trace, all of Warning, Message, Notice and Chat will be combined into verbose.

25 files changed, 171 insertions, 88 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0450ac06a..90f6f0d56 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7862,12 +7862,12 @@ bool Solver::isOutputOn(const std::string& tag) const
 
 std::ostream& Solver::getOutput(const std::string& tag) const
 {
-  // `getOutput(tag)` may raise an `OptionException`, which we do not want to
+  // `output(tag)` may raise an `OptionException`, which we do not want to
   // forward as such. We thus do not use the standard exception handling macros
   // here but roll our own.
   try
   {
-    return d_slv->getEnv().getOutput(tag);
+    return d_slv->getEnv().output(tag);
   }
   catch (const cvc5::Exception& e)
   {
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index f08d9adde..be3652dd4 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -200,8 +200,7 @@ bool solverInvoke(api::Solver* solver,
   // print output for -o raw-benchmark
   if (solver->isOutputOn("raw-benchmark"))
   {
-    std::ostream& ss = solver->getOutput("raw-benchmark");
-    cmd->toStream(ss);
+    cmd->toStream(solver->getOutput("raw-benchmark"));
   }
 
   // In parse-only mode, we do not invoke any of the commands except define-fun
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 0db16e7c6..63ca49c76 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -524,8 +524,9 @@ def generate_module_mode_impl(module):
         if option.name is None or not option.mode:
             continue
         cases = [
-            'case {type}::{enum}: return os << "{type}::{enum}";'.format(
-                type=option.type, enum=x) for x in option.mode.keys()
+            'case {type}::{enum}: return os << "{name}";'.format(
+                type=option.type, enum=enum, name=info[0]['name'])
+            for enum,info in option.mode.items()
         ]
         res.append(
             TPL_MODE_STREAM_OPERATOR.format(type=option.type,
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2a7331c67..b58063dbb 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -269,8 +269,7 @@ void OptionsHandler::enableOutputTag(const std::string& flag,
 {
   size_t tagid = static_cast<size_t>(stringToOutputTag(optarg));
   Assert(d_options->base.outputTagHolder.size() > tagid)
-      << "Trying to enable an output tag whose value is larger than the bitset "
-         "that holds it. Maybe someone forgot to update the bitset size?";
+      << "Output tag is larger than the bitset that holds it.";
   d_options->base.outputTagHolder.set(tagid);
 }
 
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 5d16c12ce..13e504835 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -64,8 +64,8 @@ void CheckModels::checkModel(TheoryModel* m,
   // Now go through all our user assertions checking if they're satisfied.
   for (const Node& assertion : al)
   {
-    Notice() << "SolverEngine::checkModel(): checking assertion " << assertion
-             << std::endl;
+    verbose(1) << "SolverEngine::checkModel(): checking assertion " << assertion
+               << std::endl;
 
     // Apply any define-funs from the problem. We do not expand theory symbols
     // like integer division here. Hence, the code below is not able to properly
@@ -73,17 +73,19 @@ void CheckModels::checkModel(TheoryModel* m,
     // is not trustworthy, since the UF introduced by expanding definitions may
     // not be properly constrained.
     Node n = sm.apply(assertion, false);
-    Notice() << "SolverEngine::checkModel(): -- substitutes to " << n
-             << std::endl;
+    verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n
+               << std::endl;
 
     n = rewrite(n);
-    Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl;
+    verbose(1) << "SolverEngine::checkModel(): -- rewrites to " << n
+               << std::endl;
 
     // We look up the value before simplifying. If n contains quantifiers,
     // this may increases the chance of finding its value before the node is
     // altered by simplification below.
     n = m->getValue(n);
-    Notice() << "SolverEngine::checkModel(): -- get value : " << n << std::endl;
+    verbose(1) << "SolverEngine::checkModel(): -- get value : " << n
+               << std::endl;
 
     if (n.isConst() && n.getConst<bool>())
     {
@@ -109,7 +111,7 @@ void CheckModels::checkModel(TheoryModel* m,
     if (!n.isConst())
     {
       // Not constant, print a less severe warning message here.
-      Warning()
+      warning()
           << "Warning : SolverEngine::checkModel(): cannot check simplified "
              "assertion : "
           << n << std::endl;
@@ -118,8 +120,8 @@ void CheckModels::checkModel(TheoryModel* m,
     }
     // Assertions that simplify to false result in an InternalError or
     // Warning being thrown below (when hardFailure is false).
-    Notice() << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
-             << std::endl;
+    verbose(1) << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
+               << std::endl;
     std::stringstream ss;
     ss << "SolverEngine::checkModel(): "
        << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl
@@ -134,13 +136,13 @@ void CheckModels::checkModel(TheoryModel* m,
     }
     else
     {
-      Warning() << ss.str() << std::endl;
+      warning() << ss.str() << std::endl;
     }
   }
   if (noCheckList.empty())
   {
-    Notice() << "SolverEngine::checkModel(): all assertions checked out OK !"
-             << std::endl;
+    verbose(1) << "SolverEngine::checkModel(): all assertions checked out OK !"
+               << std::endl;
     return;
   }
   // if the noCheckList is non-empty, we could expand definitions on this list
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index fd44c274c..dc9efdf91 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -148,7 +148,7 @@ const Printer& Env::getPrinter()
 
 std::ostream& Env::getDumpOut() { return *d_options.base.out; }
 
-bool Env::isOutputOn(options::OutputTag tag) const
+bool Env::isOutputOn(OutputTag tag) const
 {
   return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
 }
@@ -156,7 +156,12 @@ bool Env::isOutputOn(const std::string& tag) const
 {
   return isOutputOn(options::stringToOutputTag(tag));
 }
-std::ostream& Env::getOutput(options::OutputTag tag) const
+std::ostream& Env::output(const std::string& tag) const
+{
+  return output(options::stringToOutputTag(tag));
+}
+
+std::ostream& Env::output(OutputTag tag) const
 {
   if (isOutputOn(tag))
   {
@@ -164,9 +169,19 @@ std::ostream& Env::getOutput(options::OutputTag tag) const
   }
   return cvc5::null_os;
 }
-std::ostream& Env::getOutput(const std::string& tag) const
+
+bool Env::isVerboseOn(int64_t level) const
+{
+  return !Configuration::isMuzzledBuild() && d_options.base.verbosity >= level;
+}
+
+std::ostream& Env::verbose(int64_t level) const
 {
-  return getOutput(options::stringToOutputTag(tag));
+  if (isVerboseOn(level))
+  {
+    return *d_options.base.err;
+  }
+  return cvc5::null_os;
 }
 
 Node Env::evaluate(TNode n,
diff --git a/src/smt/env.h b/src/smt/env.h
index 1974408ad..25f8d0b71 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -21,7 +21,6 @@
 
 #include <memory>
 
-#include "options/base_options.h"
 #include "options/options.h"
 #include "proof/method_id.h"
 #include "theory/logic_info.h"
@@ -34,6 +33,10 @@ class StatisticsRegistry;
 class ProofNodeManager;
 class Printer;
 class ResourceManager;
+namespace options {
+enum class OutputTag;
+}
+using OutputTag = options::OutputTag;
 
 namespace context {
 class Context;
@@ -152,25 +155,41 @@ class Env
    * Check whether the output for the given output tag is enabled. Output tags
    * are enabled via the `output` option (or `-o` on the command line).
    */
-  bool isOutputOn(options::OutputTag tag) const;
+  bool isOutputOn(OutputTag tag) const;
   /**
    * Check whether the output for the given output tag (as a string) is enabled.
    * Output tags are enabled via the `output` option (or `-o` on the command
    * line).
    */
   bool isOutputOn(const std::string& tag) const;
+
+  /**
+   * Return the output stream for the given output tag (as a string). If the
+   * output tag is enabled, this returns the output stream from the `out`
+   * option. Otherwise, a null stream (`cvc5::null_os`) is returned.
+   */
+  std::ostream& output(const std::string& tag) const;
+
   /**
    * Return the output stream for the given output tag. If the output tag is
    * enabled, this returns the output stream from the `out` option. Otherwise,
-   * a null stream (`cvc5::null_os`) is returned.
+   * a null stream (`cvc5::null_os`) is returned. The user of this method needs
+   * to make sure that a proper S-expression is printed.
    */
-  std::ostream& getOutput(options::OutputTag tag) const;
+  std::ostream& output(OutputTag tag) const;
+
   /**
-   * Return the output stream for the given output tag (as a string). If the
-   * output tag is enabled, this returns the output stream from the `out`
-   * option. Otherwise, a null stream (`cvc5::null_os`) is returned.
+   * Check whether the verbose output for the given verbosity level is enabled.
+   * The verbosity level is raised (or lowered) with the `-v` (or `-q`) option.
+   */
+  bool isVerboseOn(int64_t level) const;
+
+  /**
+   * Return the output stream for the given verbosity level. If the verbosity
+   * level is enabled, this returns the output stream from the `err` option.
+   * Otherwise, a null stream (`cvc5::null_os`) is returned.
    */
-  std::ostream& getOutput(const std::string& tag) const;
+  std::ostream& verbose(int64_t level) const;
 
   /* Rewrite helpers--------------------------------------------------------- */
   /**
diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp
index 926bf61ff..8af3bdfd0 100644
--- a/src/smt/env_obj.cpp
+++ b/src/smt/env_obj.cpp
@@ -70,4 +70,20 @@ StatisticsRegistry& EnvObj::statisticsRegistry() const
   return d_env.getStatisticsRegistry();
 }
 
+bool EnvObj::isOutputOn(OutputTag tag) const { return d_env.isOutputOn(tag); }
+
+std::ostream& EnvObj::output(OutputTag tag) const { return d_env.output(tag); }
+
+bool EnvObj::isVerboseOn(int64_t level) const
+{
+  return d_env.isVerboseOn(level);
+}
+
+std::ostream& EnvObj::verbose(int64_t level) const
+{
+  return d_env.verbose(level);
+}
+
+std::ostream& EnvObj::warning() const { return verbose(0); }
+
 }  // namespace cvc5
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
index b240b4852..2c88f45b4 100644
--- a/src/smt/env_obj.h
+++ b/src/smt/env_obj.h
@@ -22,7 +22,6 @@
 #include <memory>
 
 #include "expr/node.h"
-
 namespace cvc5 {
 
 class Env;
@@ -35,6 +34,10 @@ namespace context {
 class Context;
 class UserContext;
 }  // namespace context
+namespace options {
+enum class OutputTag;
+}
+using OutputTag = options::OutputTag;
 
 class EnvObj
 {
@@ -88,6 +91,21 @@ class EnvObj
   /** Get the statistics registry via Env. */
   StatisticsRegistry& statisticsRegistry() const;
 
+  /** Convenience wrapper for Env::isOutputOn(). */
+  bool isOutputOn(OutputTag tag) const;
+
+  /** Convenience wrapper for Env::output(). */
+  std::ostream& output(OutputTag tag) const;
+
+  /** Convenience wrapper for Env::isVerboseOn(). */
+  bool isVerboseOn(int64_t level) const;
+
+  /** Convenience wrapper for Env::verbose(). */
+  std::ostream& verbose(int64_t) const;
+
+  /** Convenience wrapper for Env::verbose(0). */
+  std::ostream& warning() const;
+
   /** The associated environment. */
   Env& d_env;
 };
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 2ffa0d7c1..919368512 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -79,9 +79,9 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
   {
     if (r.asSatisfiabilityResult().isSat() != Result::SAT && doFull)
     {
-      Notice()
+      verbose(1)
           << "While performing quantifier elimination, unexpected result : "
-          << r << " for query.";
+          << r << " for query." << std::endl;
       // failed, return original
       return q;
     }
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index c7147a676..fddea7649 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1383,7 +1383,8 @@ std::vector<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& core)
   Assert(options::unsatCores())
       << "cannot reduce unsat core if unsat cores are turned off";
 
-  Notice() << "SolverEngine::reduceUnsatCore(): reducing unsat core" << endl;
+  d_env->verbose(1) << "SolverEngine::reduceUnsatCore(): reducing unsat core"
+                    << std::endl;
   std::unordered_set<Node> removed;
   for (const Node& skip : core)
   {
@@ -1450,7 +1451,8 @@ void SolverEngine::checkUnsatCore()
   Assert(d_env->getOptions().smt.unsatCores)
       << "cannot check unsat core if unsat cores are turned off";
 
-  Notice() << "SolverEngine::checkUnsatCore(): generating unsat core" << endl;
+  d_env->verbose(1) << "SolverEngine::checkUnsatCore(): generating unsat core"
+                    << std::endl;
   UnsatCore core = getUnsatCore();
 
   // initialize the core checker
@@ -1468,14 +1470,15 @@ void SolverEngine::checkUnsatCore()
     coreChecker->declareSepHeap(sepLocType, sepDataType);
   }
 
-  Notice() << "SolverEngine::checkUnsatCore(): pushing core assertions"
-           << std::endl;
+  d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core assertions"
+                    << std::endl;
   theory::TrustSubstitutionMap& tls = d_env->getTopLevelSubstitutions();
   for (UnsatCore::iterator i = core.begin(); i != core.end(); ++i)
   {
     Node assertionAfterExpansion = tls.apply(*i, false);
-    Notice() << "SolverEngine::checkUnsatCore(): pushing core member " << *i
-             << ", expanded to " << assertionAfterExpansion << "\n";
+    d_env->verbose(1) << "SolverEngine::checkUnsatCore(): pushing core member "
+                      << *i << ", expanded to " << assertionAfterExpansion
+                      << std::endl;
     coreChecker->assertFormula(assertionAfterExpansion);
   }
   Result r;
@@ -1487,7 +1490,8 @@ void SolverEngine::checkUnsatCore()
   {
     throw;
   }
-  Notice() << "SolverEngine::checkUnsatCore(): result is " << r << endl;
+  d_env->verbose(1) << "SolverEngine::checkUnsatCore(): result is " << r
+                    << std::endl;
   if (r.asSatisfiabilityResult().isUnknown())
   {
     Warning() << "SolverEngine::checkUnsatCore(): could not check core result "
@@ -1511,7 +1515,8 @@ void SolverEngine::checkModel(bool hardFailure)
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
 
-  Notice() << "SolverEngine::checkModel(): generating model" << endl;
+  d_env->verbose(1) << "SolverEngine::checkModel(): generating model"
+                    << std::endl;
   TheoryModel* m = getAvailableModel("check model");
   Assert(m != nullptr);
 
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 5db9804c6..4c8d3e5bd 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -257,8 +257,11 @@ void SygusSolver::checkSynthSolution(Assertions& as)
 {
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
-  Notice() << "SygusSolver::checkSynthSolution(): checking synthesis solution"
-           << std::endl;
+  if (isVerboseOn(1))
+  {
+    verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution"
+               << std::endl;
+  }
   std::map<Node, std::map<Node, Node>> sol_map;
   // Get solutions and build auxiliary vectors for substituting
   QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
@@ -308,13 +311,19 @@ void SygusSolver::checkSynthSolution(Assertions& as)
   std::unordered_map<Node, Node> cache;
   for (const Node& assertion : alist)
   {
-    Notice() << "SygusSolver::checkSynthSolution(): checking assertion "
-             << assertion << std::endl;
+    if (isVerboseOn(1))
+    {
+      verbose(1) << "SyGuS::checkSynthSolution: checking assertion "
+                 << assertion << std::endl;
+    }
     Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
     // Apply any define-funs from the problem.
     Node n = d_smtSolver.getPreprocessor()->expandDefinitions(assertion, cache);
-    Notice() << "SygusSolver::checkSynthSolution(): -- expands to " << n
-             << std::endl;
+    if (isVerboseOn(1))
+    {
+      verbose(1) << "SyGuS::checkSynthSolution: -- expands to " << n
+                 << std::endl;
+    }
     Trace("check-synth-sol") << "Expanded assertion " << n << "\n";
     if (conjs.find(n) == conjs.end())
     {
@@ -364,8 +373,12 @@ void SygusSolver::checkSynthSolution(Assertions& as)
       conjBody = conjBody.substitute(
           vars.begin(), vars.end(), skos.begin(), skos.end());
     }
-    Notice() << "SygusSolver::checkSynthSolution(): -- body substitutes to "
-             << conjBody << std::endl;
+
+    if (isVerboseOn(1))
+    {
+      verbose(1) << "SyGuS::checkSynthSolution: -- body substitutes to "
+                 << conjBody << std::endl;
+    }
     Trace("check-synth-sol")
         << "Substituted body of assertion to " << conjBody << "\n";
     solChecker->assertFormula(conjBody);
@@ -381,8 +394,10 @@ void SygusSolver::checkSynthSolution(Assertions& as)
       solChecker->assertFormula(ar);
     }
     Result r = solChecker->checkSat();
-    Notice() << "SygusSolver::checkSynthSolution(): result is " << r
-             << std::endl;
+    if (isVerboseOn(1))
+    {
+      verbose(1) << "SyGuS::checkSynthSolution: result is " << r << std::endl;
+    }
     Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
     if (r.asSatisfiabilityResult().isUnknown())
     {
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index fe48aa59d..1c6e3f0cb 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -382,9 +382,7 @@ void TheoryDatatypes::postCheck(Effort level)
   }
 
   Trace("datatypes-check") << "Finished check effort " << level << std::endl;
-  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
-    Notice() << "TheoryDatatypes::check(): done" << endl;
-  }
+  Debug("datatypes") << "TheoryDatatypes::check(): done" << std::endl;
 }
 
 bool TheoryDatatypes::needsCheckLastEffort() {
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index f4370c017..0c9a5ba46 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -172,9 +172,9 @@ TrustNode AlphaEquivalence::reduceQuantifier(Node q)
   lem = ret.eqNode(q);
   if (q.getNumChildren() == 3)
   {
-    Notice() << "Ignoring annotated quantified formula based on alpha "
-                "equivalence: "
-             << q << std::endl;
+    verbose(1) << "Ignoring annotated quantified formula based on alpha "
+                  "equivalence: "
+               << q << std::endl;
   }
   // if successfully computed the substitution above
   if (isProofEnabled() && !vars.empty())
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index fdb0d0db3..f1d80032b 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -153,10 +153,9 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
         && d_auto_gen_trigger[1][f].empty() && !QuantAttributes::hasPattern(f))
     {
       Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
-      if (d_env.isOutputOn(options::OutputTag::TRIGGER))
+      if (isOutputOn(OutputTag::TRIGGER))
       {
-        d_env.getOutput(options::OutputTag::TRIGGER)
-            << "(no-trigger " << f << ")" << std::endl;
+        output(OutputTag::TRIGGER) << "(no-trigger " << f << ")" << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index ff02e5f3e..e267b470d 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -78,12 +78,11 @@ Trigger::Trigger(Env& env,
     extNodes.push_back(ns);
   }
   d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes);
-  if (d_env.isOutputOn(options::OutputTag::TRIGGER))
+  if (isOutputOn(OutputTag::TRIGGER))
   {
     QuantAttributes& qa = d_qreg.getQuantAttributes();
-    d_env.getOutput(options::OutputTag::TRIGGER)
-        << "(trigger " << qa.quantToString(q) << " " << d_trNode << ")"
-        << std::endl;
+    output(OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q) << " "
+                               << d_trNode << ")" << std::endl;
   }
   QuantifiersStatistics& stats = qs.getStats();
   if( d_nodes.size()==1 ){
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 23f789f4e..1af2b3f75 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -706,7 +706,7 @@ void Instantiate::notifyEndRound()
           << " * " << i.second << " for " << i.first << std::endl;
     }
   }
-  if (d_env.isOutputOn(options::OutputTag::INST))
+  if (isOutputOn(OutputTag::INST))
   {
     bool req = !options().printer.printInstFull;
     for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
@@ -716,9 +716,8 @@ void Instantiate::notifyEndRound()
       {
         continue;
       }
-      d_env.getOutput(options::OutputTag::INST)
-          << "(num-instantiations " << name << " " << i.second << ")"
-          << std::endl;
+      output(OutputTag::INST) << "(num-instantiations " << name << " "
+                              << i.second << ")" << std::endl;
     }
   }
 }
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6c3f5e70b..1fde43913 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -372,7 +372,7 @@ bool SynthConjecture::doCheck()
     }
   }
 
-  bool printDebug = d_env.isOutputOn(options::OutputTag::SYGUS);
+  bool printDebug = isOutputOn(OutputTag::SYGUS);
   if (!constructed_cand)
   {
     // get the model value of the relevant terms from the master module
@@ -437,9 +437,9 @@ bool SynthConjecture::doCheck()
           }
         }
         Trace("sygus-engine") << std::endl;
-        if (d_env.isOutputOn(options::OutputTag::SYGUS))
+        if (d_env.isOutputOn(OutputTag::SYGUS))
         {
-          d_env.getOutput(options::OutputTag::SYGUS)
+          d_env.output(OutputTag::SYGUS)
               << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
         }
       }
@@ -518,16 +518,15 @@ bool SynthConjecture::doCheck()
   // print the candidate solution for debugging
   if (constructed_cand && printDebug)
   {
-    const Options& sopts = options();
-    std::ostream& out = *sopts.base.out;
+    std::ostream& out = output(OutputTag::SYGUS);
     out << "(sygus-candidate ";
     Assert(d_quant[0].getNumChildren() == candidate_values.size());
     for (size_t i = 0, ncands = candidate_values.size(); i < ncands; i++)
     {
       Node v = candidate_values[i];
-      std::stringstream ss;
-      TermDbSygus::toStreamSygus(ss, v);
-      out << "(" << d_quant[0][i] << " " << ss.str() << ")";
+      out << "(" << d_quant[0][i] << " ";
+      TermDbSygus::toStreamSygus(out, v);
+      out << ")";
     }
     out << ")" << std::endl;
   }
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 08fab59eb..2fc7f0c29 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -815,10 +815,11 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr, std::ostream& out)
     }
     if (!ptDisequalConst)
     {
-      Notice() << "Warning: " << bv << " and " << bvr
-               << " evaluate to different (non-constant) values on point:"
-               << std::endl;
-      Notice() << ptOut.str();
+      d_env.verbose(1)
+          << "Warning: " << bv << " and " << bvr
+          << " evaluate to different (non-constant) values on point:"
+          << std::endl;
+      d_env.verbose(1) << ptOut.str();
       return;
     }
     // we have detected unsoundness in the rewriter
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 03880bfbb..5aafae367 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1892,7 +1892,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
               // assertions with unevaluable operators, e.g. transcendental
               // functions. It also may happen for separation logic, where
               // check-model support is limited.
-              Warning() << ss.str();
+              warning() << ss.str();
             }
           }
         }
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 650ef1d70..83862e8bb 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -828,7 +828,6 @@ void SortModel::getDisequalitiesToRegions(int ri,
       for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
         if( (*it2).second ){
           Assert(isValid(d_regions_map[(*it2).first]));
-          //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
           regions_diseq[ d_regions_map[ (*it2).first ] ]++;
         }
       }
@@ -1046,7 +1045,6 @@ int SortModel::addSplit(Region* r)
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
     //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
     //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
-    //Notice() << "*** Split on " << s << std::endl;
     //split on the equality s
     Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
     // send lemma, with caching
diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2
index 6b07dfc1c..24e05ec2a 100644
--- a/test/regress/regress0/options/set-and-get-options.smt2
+++ b/test/regress/regress0/options/set-and-get-options.smt2
@@ -3,7 +3,7 @@
 ; EXPECT: true
 ; EXPECT: false
 ; EXPECT: 15
-; EXPECT: SimplificationMode::NONE
+; EXPECT: none
 
 (get-option :command-verbosity)
 (set-option :command-verbosity (* 1))
diff --git a/test/regress/regress0/sygus/issue5512-vvv.sy b/test/regress/regress0/sygus/issue5512-vvv.sy
index 9d37032ac..333c0dd5a 100644
--- a/test/regress/regress0/sygus/issue5512-vvv.sy
+++ b/test/regress/regress0/sygus/issue5512-vvv.sy
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts
+; ERROR-SCRUBBER: sed -e 's/.*//g'
 ; SCRUBBER: sed -e 's/.*//g'
 ; EXIT: 0
 
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 4c9ec4c0d..f89ecfffd 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1429,7 +1429,7 @@ class SolverTest
       assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class));
       OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo();
       assertions.add(() -> assertEquals("NONE", modeInfo.getDefaultValue()));
-      assertions.add(() -> assertEquals("OutputTag::NONE", modeInfo.getCurrentValue()));
+      assertions.add(() -> assertEquals("none", modeInfo.getCurrentValue()));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("NONE")));
     }
     assertAll(assertions);
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 062a2a59e..eca6683ba 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1379,7 +1379,7 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
     auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
     EXPECT_EQ("NONE", modeInfo.defaultValue);
-    EXPECT_EQ("OutputTag::NONE", modeInfo.currentValue);
+    EXPECT_EQ("none", modeInfo.currentValue);
     EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "NONE")
                 != modeInfo.modes.end());
   }