1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 2a8994c25..8f0eea58f 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -50,8 +50,12 @@ class SynthEngine : public QuantifiersModule
    * this is the quantifier elimination step option::sygusQePreproc().
    */
   void assignConjecture(Node q);
-  /** check conjecture */
-  void checkConjecture(SynthConjecture* conj);
+  /** check conjecture
+   *
+   * This method returns true if the conjecture is finished processing solutions
+   * for this call to SynthEngine::check().
+   */
+  bool checkConjecture(SynthConjecture* conj);
 
  public:
   SynthEngine(QuantifiersEngine* qe, context::Context* c);