diff options
| author | ajreynol <reynolds@laraserver2.epfl.ch> | 2014-06-14 09:40:49 +0200 |
|---|---|---|
| committer | ajreynol <reynolds@laraserver2.epfl.ch> | 2014-06-14 09:40:56 +0200 |
| commit | 7bb688ad25823ef140d282d6e2f05ad5fb953f74 (patch) | |
| tree | a58618093531cd80dabfbc35a482d1b572c2990b /src/theory/rep_set.cpp | |
| parent | 8c45a2ef94d68ceff7c0997e80d5b573895f2f69 (diff) | |
Fix for fmf with large finite cardinalities.
Diffstat (limited to 'src/theory/rep_set.cpp')
| -rw-r--r-- | src/theory/rep_set.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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; |