From 7bb688ad25823ef140d282d6e2f05ad5fb953f74 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 14 Jun 2014 09:40:49 +0200 Subject: [PATCH] Fix for fmf with large finite cardinalities. --- src/theory/rep_set.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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; -- 2.30.2