From 854c414f056e306dd8678fd7459ee9dee8b8d6b3 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Dec 2018 17:00:58 -0600
Subject: [PATCH]  Skip non-cardinality types in sets min card inference
 (#2734)

---
 src/theory/sets/theory_sets_private.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

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() ){
-- 
2.30.2