I made a documentation change to get() to make explicit the contract requirements...

diff --git a/src/theory/theory.h b/src/theory/theory.h
index bdd695cdd3d56fc8871c5f30f9cd9e4fc34773e6..1bf6f660c532b6b1dcbf17c6e4d55878667230a3 100644 (file)
--- 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;