diff options
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 83c66c2d3..1c302573e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1543,6 +1543,12 @@ void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) { for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){ Node eqc = d_set_eqc[i]; + TypeNode tn = eqc.getType().getSetElementType(); + if (d_t_card_enabled.find(tn) == d_t_card_enabled.end()) + { + // cardinality is not enabled for this type, skip + continue; + } //get members in class std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc ); if( itm!=d_pol_mems[0].end() ){ |