Fix for fmf with large finite cardinalities.

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 7dd8d02f62c23472bef7e69b7e448c6f89480c58..e7370311d7c16cb796c9be24e08e7c31a986d2cb 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -169,7 +169,8 @@ bool RepSetIterator::initialize(){
         }
       }
     //enumerate if the sort is reasonably small, the upper bound of 1000 is chosen arbitrarily for now
-    }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){
+    }else if( tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() &&
+              tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){
       d_rep_set->complete( tn );
     }else{
       Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;