summaryrefslogtreecommitdiff
path: root/test/regress/regress1/rels/bv1-unitb.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/rels/bv1-unitb.cvc')
-rw-r--r--test/regress/regress1/rels/bv1-unitb.cvc22
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress1/rels/bv1-unitb.cvc b/test/regress/regress1/rels/bv1-unitb.cvc
deleted file mode 100644
index 0a09614a7..000000000
--- a/test/regress/regress1/rels/bv1-unitb.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% EXPECT: unsat
-OPTION "logic" "ALL";
-DATATYPE unitb = ub(data : BITVECTOR(1)) END;
-BvPair: TYPE = [BITVECTOR(1), unitb, 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);
-u : unitb;
-
-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