Fixes for quantifiers documentation (#3811)

Minor fixes discovered during development of sygus-inst.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index a4f4af2e8..126facfa8 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -59,6 +59,13 @@ class EnumValGenerator
    * Increment this value generator. If this returns false, then we are out of
    * values. If this returns true, getCurrent(), if non-null, returns the
    * current term.
+   *
+   * Notice that increment() may return true and afterwards it may be the case
+   * getCurrent() is null. We do this so that increment() does not take too
+   * much time per call, which can be the case for grammars where it is
+   * difficult to find the next (non-redundant) term. Returning true with
+   * a null current term gives the caller the chance to interleave other
+   * reasoning.
    */
   virtual bool increment() = 0;
   /** Get the current concrete value generated by this class. */