Bug fix for rep-set.

(Cherry-picked from commit c71ec27 in master.)

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 3b5ba0cef5f5240eee712590d1712da6cfdd1573..3057e4a93e07523c77e01711bc363187410b65fe 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -135,16 +135,9 @@ bool RepSetIterator::initialize(){
     }else if( tn.isInteger() || tn.isReal() ){
       Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
       d_incomplete = true;
-    }else if( tn.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      //if finite, then complete all values of the domain
-      if( dt.isFinite() ){
-        d_rep_set->complete( tn );
-        //d_incomplete = true;
-      }else{
-        Trace("fmf-incomplete") << "Incomplete because of infinite datatype " << tn << std::endl;
-        d_incomplete = true;
-      }
+    //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
+    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
+      d_rep_set->complete( tn );
     }else{
       Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
       d_incomplete = true;