summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rels/bv1-unit.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/rels/bv1-unit.cvc')
-rw-r--r--test/regress/regress0/rels/bv1-unit.cvc21
1 files changed, 0 insertions, 21 deletions
diff --git a/test/regress/regress0/rels/bv1-unit.cvc b/test/regress/regress0/rels/bv1-unit.cvc
deleted file mode 100644
index 970ebdc8c..000000000
--- a/test/regress/regress0/rels/bv1-unit.cvc
+++ /dev/null
@@ -1,21 +0,0 @@
-% EXPECT: unsat
-OPTION "logic" "ALL_SUPPORTED";
-DATATYPE unit = u END;
-BvPair: TYPE = [BITVECTOR(1), unit, BITVECTOR(1)];
-x : SET OF BvPair;
-y : SET OF BvPair;
-
-a : BITVECTOR(1);
-b : BITVECTOR(1);
-c : BITVECTOR(1);
-d : BITVECTOR(1);
-e : BITVECTOR(1);
-
-ASSERT NOT ( b = c );
-
-ASSERT (a, u, b) IS_IN x;
-ASSERT (a, u, c) IS_IN x;
-ASSERT (d, u, a) IS_IN y;
-ASSERT NOT ( ( a, u, u, a ) IS_IN (x JOIN y));
-
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback