diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-03 13:44:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-03 13:44:37 -0500 |
| commit | e223134343162e5c2d5e65c34ac74540d326b37d (patch) | |
| tree | 65acbab5671dc90bec6790f6a70be76e16fe037a /src/theory/quantifiers/sygus | |
| parent | 9f95889dd0853a249c4e01f82174704cf2bc628c (diff) | |
| parent | c56eaf4423fbf65663a4e03c8a60ed937c99de7d (diff) | |
Merge branch 'master' into fixStrRegressfixStrRegress
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 4e8d7d46d..b2b69687c 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -20,6 +20,7 @@ #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" @@ -384,7 +385,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) } } - bool printDebug = options::debugSygus(); + bool printDebug = Output.isOn(options::OutputTag::SYGUS); if (!constructed_cand) { // get the model value of the relevant terms from the master module @@ -454,12 +455,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) } } Trace("sygus-engine") << std::endl; - if (printDebug) - { - Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.base.out; - out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; - } + Output(options::OutputTag::SYGUS) + << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( |