summaryrefslogtreecommitdiff
path: root/test/regress/regress1/rels/bv1p-sat.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/rels/bv1p-sat.cvc')
-rw-r--r--test/regress/regress1/rels/bv1p-sat.cvc22
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress1/rels/bv1p-sat.cvc b/test/regress/regress1/rels/bv1p-sat.cvc
deleted file mode 100644
index a48cb6407..000000000
--- a/test/regress/regress1/rels/bv1p-sat.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL";
-BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
-x : SET OF BvPair;
-y : SET OF BvPair;
-
-a : BvPair;
-b : BvPair;
-c : BvPair;
-d : BvPair;
-
-ASSERT DISTINCT ( a, b );
-ASSERT DISTINCT ( c, d );
-
-ASSERT a IS_IN x;
-ASSERT b IS_IN x;
-ASSERT a IS_IN y;
-ASSERT b IS_IN y;
-ASSERT NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y));
-
-
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback