Skip non-cardinality types in sets min card inference (#2734)

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 83c66c2d32b6102dfcddc747ed1f84f356d5583c..1c302573e036cb414237214896e04ae87c2da62a 100644 (file)
--- 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() ){