summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rels/join-eq-u-sat.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/rels/join-eq-u-sat.cvc')
-rw-r--r--test/regress/regress0/rels/join-eq-u-sat.cvc22
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress0/rels/join-eq-u-sat.cvc b/test/regress/regress0/rels/join-eq-u-sat.cvc
deleted file mode 100644
index 1c45aa46b..000000000
--- a/test/regress/regress0/rels/join-eq-u-sat.cvc
+++ /dev/null
@@ -1,22 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL";
-IntPair: TYPE = [INT, INT];
-x : SET OF IntPair;
-y : SET OF IntPair;
-DATATYPE unit = u END;
-IntUPair: TYPE = [INT, unit];
-UIntPair: TYPE = [unit, INT];
-w : SET OF IntUPair;
-z : SET OF UIntPair;
-
-ASSERT (x JOIN y) = (w JOIN z);
-
-ASSERT (0,1) IS_IN (x JOIN y);
-ASSERT (0,u) IS_IN w;
-
-t : INT;
-ASSERT t > 0 AND t < 3;
-
-ASSERT NOT (u, t ) IS_IN z;
-
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback