diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e4ec40325..62c61fe1e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -444,7 +444,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) if (printDebug) { Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.getOut(); + std::ostream& out = *sopts.base.out; out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; } } @@ -529,7 +529,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) if (printDebug) { Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.getOut(); + std::ostream& out = *sopts.base.out; out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++) @@ -995,7 +995,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, // we have generated a solution, print it // get the current output stream Options& sopts = smt::currentSmtEngine()->getOptions(); - printSynthSolutionInternal(*sopts.getOut()); + printSynthSolutionInternal(*sopts.base.out); excludeCurrentSolution(enums, values); } |