Eliminate Output macro in favor of simple Env functions (#7223)

[cvc5.git] / src / theory / quantifiers / sygus / synth_conjecture.cpp

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 22ba879d7dd31d74f1b42e420bf83543aef1f04c..ab2a73cb0adf8bcdd22a26d8ecd9e5aaf7a36de4 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -20,7 +20,6 @@
 #include "expr/skolem_manager.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
-#include "options/outputc.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "smt/logic_exception.h"
@@ -359,7 +358,7 @@ bool SynthConjecture::doCheck()
     }
   }
 
-  bool printDebug = Output.isOn(options::OutputTag::SYGUS);
+  bool printDebug = d_env.isOutputOn(options::OutputTag::SYGUS);
   if (!constructed_cand)
   {
     // get the model value of the relevant terms from the master module
@@ -424,8 +423,11 @@ bool SynthConjecture::doCheck()
           }
         }
         Trace("sygus-engine") << std::endl;
-        Output(options::OutputTag::SYGUS)
-            << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
+        if (d_env.isOutputOn(options::OutputTag::SYGUS))
+        {
+          d_env.getOutput(options::OutputTag::SYGUS)
+              << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
+        }
       }
       Assert(candidate_values.empty());
       constructed_cand = d_master->constructCandidates(