From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Dec 2018 23:00:58 +0000 (-0600)
Subject:  Skip non-cardinality types in sets min card inference (#2734)
X-Git-Tag: cvc5-1.0.0~4338
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=854c414f056e306dd8678fd7459ee9dee8b8d6b3;p=cvc5.git

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