Fix minor bug in sets rewriter

As reported by Coverity, one of the switches in the sets rewriter had a missing
break. This could lead to an assertion failure when rewriting the cardinality
of a transpose as in the test case included in this commit.

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 3590fc62d6061ec1df15ca1a4da242dce9d626d6..e42a3347d6903ac87d4e1d1aacdb02f59b87bfa0 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -328,6 +328,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
                    NodeManager::currentNM()->mkNode( kind::CARD, NodeManager::currentNM()->mkNode( kind::INTERSECTION, node[0][0], node[0][1] ) ) );                                      
       return RewriteResponse(REWRITE_DONE, ret );
     }
+    break;
   }
   case kind::TRANSPOSE: {
     if(node[0].getKind() == kind::TRANSPOSE) {

diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
index d1c035371e251dd584adc2fbcc135a9dca2731da..7f772a8e17eaa5cc4580d19037f26a8c9db671d4 100644 (file)
--- a/test/regress/regress0/rels/Makefile.am
+++ b/test/regress/regress0/rels/Makefile.am
@@ -112,7 +112,8 @@ TESTS =     \
   joinImg_1_1.cvc \
   joinImg_1.cvc \
   joinImg_2_1.cvc \
-  joinImg_2.cvc  
+  joinImg_2.cvc \
+  card_transpose.cvc
 
 # unsolved : garbage_collect.cvc
 

diff --git a/test/regress/regress0/rels/card_transpose.cvc b/test/regress/regress0/rels/card_transpose.cvc
new file mode 100644 (file)
index 0000000..bde7fe5
--- /dev/null
+++ b/test/regress/regress0/rels/card_transpose.cvc
@@ -0,0 +1,6 @@
+% EXPECT: unknown (INCOMPLETE)
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+ASSERT (CARD(TRANSPOSE(x)) > 0);
+CHECKSAT;