summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/synth_conjecture.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp6
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback