summaryrefslogtreecommitdiff
path: root/test/regress/regress1/rels/join-eq-structure_0_1.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/rels/join-eq-structure_0_1.cvc')
-rw-r--r--test/regress/regress1/rels/join-eq-structure_0_1.cvc26
1 files changed, 0 insertions, 26 deletions
diff --git a/test/regress/regress1/rels/join-eq-structure_0_1.cvc b/test/regress/regress1/rels/join-eq-structure_0_1.cvc
deleted file mode 100644
index e27d3811c..000000000
--- a/test/regress/regress1/rels/join-eq-structure_0_1.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL_SUPPORTED";
-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) OR (x JOIN y ) = TRANSPOSE(w JOIN z);
-
-ASSERT (0,1) IS_IN (x JOIN y);
-
-t : INT;
-ASSERT t >= 0 AND t <=1;
-s : INT;
-ASSERT s >= 0 AND s <=1;
-
-ASSERT s+t = 1;
-
-ASSERT ( s ,u ) IS_IN w;
-ASSERT NOT ( u, t ) IS_IN z;
-
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback