add isFinished() to type enumerators (so we don't rely on exception-throwing after exhaustively enumerating finite types), also fix a standards-related FIXME in SmtEngine by clarifying the text of an error message

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index e62baa2f6..4dd139be7 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -72,6 +72,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return false;
+  }
+
 };/* class RationalEnumerator */
 
 class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
@@ -100,6 +104,10 @@ public:
     return *this;
   }
 
+  bool isFinished() throw() {
+    return false;
+  }
+
 };/* class IntegerEnumerator */
 
 }/* CVC4::theory::arith namespace */