From 816630a9e9e6b13f7299535a18fe87c5f8180def Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 6 Feb 2013 21:30:35 -0500
Subject: [PATCH] make datatypes enumerator behavior clearer (no exceptions in
 normal operation)

---
 src/theory/datatypes/type_enumerator.h | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 2a14d7fba..8ee275f70 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -139,11 +139,10 @@ public:
   DatatypesEnumerator& operator++() throw() {
     if(d_ctor < d_datatype.getNumConstructors()) {
       for(size_t a = d_datatype[d_ctor].getNumArgs(); a > 0; --a) {
-        try {
-          *++*d_argEnumerators[a - 1];
-          return *this;
-        } catch(NoMoreValuesException&) {
+        if((++*d_argEnumerators[a - 1]).isFinished()) {
           *d_argEnumerators[a - 1] = TypeEnumerator(Node::fromExpr(d_datatype[d_ctor][a - 1].getSelector()).getType()[1]);
+        } else {
+          return *this;
         }
       }
 
-- 
2.30.2