summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-05-15 11:56:43 -0500
committerGitHub <noreply@github.com>2017-05-15 11:56:43 -0500
commitf6215a3d10c11976cffbeb4c88223e8434ffc4d3 (patch)
tree828a7f4eddc1e2b096bad8049e7ba6dddbbc8872 /test
parentb3f716fc402e2508a2ae1183fcfebebd2c95d6a3 (diff)
parentfdef54aaa36793cb9314dea3830879e051db2aa8 (diff)
Merge pull request #158 from 4tXJ7f/fix_sets_rewriter
Fix minor bug in sets rewriter
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/rels/Makefile.am3
-rw-r--r--test/regress/regress0/rels/card_transpose.cvc6
2 files changed, 8 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback