From: Andres Noetzli <noetzli@stanford.edu>
Date: Mon, 15 May 2017 16:50:45 +0000 (-0700)
Subject: Fix minor bug in sets rewriter
X-Git-Tag: cvc5-1.0.0~5800^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fdef54aaa36793cb9314dea3830879e051db2aa8;p=cvc5.git

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 3590fc62d..e42a3347d 100644
--- 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 d1c035371..7f772a8e1 100644
--- 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
index 000000000..bde7fe53e
--- /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;