summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus')
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index fc1bda579..43051eb99 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -136,8 +136,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
activeCheckConj.clear();
activeCheckConj = acnext;
acnext.clear();
- } while (!activeCheckConj.empty()
- && !d_quantEngine->theoryEngineNeedsCheck());
+ } while (!activeCheckConj.empty() && !d_qstate.getValuation().needCheck());
Trace("sygus-engine")
<< "Finished Counterexample Guided Instantiation engine." << std::endl;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback