summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/query_generator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/query_generator.cpp')
-rw-r--r--src/theory/quantifiers/query_generator.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 99e7b5a8c..248128c1e 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -146,7 +146,8 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
{
// external query
- if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_ALL)
+ if (options::sygusQueryGenDumpFiles()
+ == options::SygusQueryDumpFilesMode::ALL)
{
dumpQuery(qy, spIndex);
}
@@ -179,7 +180,8 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
ss << "but CVC4 answered unsat!" << std::endl;
AlwaysAssert(false) << ss.str();
}
- if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_UNSOLVED)
+ if (options::sygusQueryGenDumpFiles()
+ == options::SygusQueryDumpFilesMode::UNSOLVED)
{
if (r.asSatisfiabilityResult().isSat() != Result::SAT)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback