From: ajreynol <reynolds@laraserver2.epfl.ch>
Date: Sat, 14 Jun 2014 07:40:49 +0000 (+0200)
Subject: Fix for fmf with large finite cardinalities.
X-Git-Tag: cvc5-1.0.0~6818
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7bb688ad25823ef140d282d6e2f05ad5fb953f74;p=cvc5.git

Fix for fmf with large finite cardinalities.
---

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 7dd8d02f6..e7370311d 100644
--- 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;