I made a documentation change to get() to make explicit the contract requirements for 'slurping the queue'. Closes bug 154

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index bdd695cdd..1bf6f660c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -264,6 +264,12 @@ public:
 
   /**
    * Check the current assignment's consistency.
+   *
+   * An implementation of check() is required to either:
+   * - return a conflict on the output channel,
+   * - be interrupted,
+   * - throw an exception
+   * - or call get() until done() is true.
    */
   virtual void check(Effort level = FULL_EFFORT) = 0;