summaryrefslogtreecommitdiff
path: root/test/regress/regress0/rels/rel_complex_1.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/rels/rel_complex_1.cvc')
-rw-r--r--test/regress/regress0/rels/rel_complex_1.cvc34
1 files changed, 0 insertions, 34 deletions
diff --git a/test/regress/regress0/rels/rel_complex_1.cvc b/test/regress/regress0/rels/rel_complex_1.cvc
deleted file mode 100644
index 4b23cdd2b..000000000
--- a/test/regress/regress0/rels/rel_complex_1.cvc
+++ /dev/null
@@ -1,34 +0,0 @@
-% EXPECT: unsat
-OPTION "logic" "ALL";
-IntPair: TYPE = [INT, INT];
-IntTup: TYPE = [INT];
-x : SET OF IntPair;
-y : SET OF IntPair;
-r : SET OF IntPair;
-
-w : SET OF IntTup;
-z : SET OF IntTup;
-r2 : SET OF IntPair;
-
-a : IntPair;
-ASSERT a = (3,1);
-ASSERT a IS_IN x;
-
-d : IntPair;
-ASSERT d = (1,3);
-ASSERT d IS_IN y;
-
-e : IntPair;
-ASSERT e = (4,3);
-ASSERT r = (x JOIN y);
-
-ASSERT TUPLE(1) IS_IN w;
-ASSERT TUPLE(2) IS_IN z;
-ASSERT r2 = (w PRODUCT z);
-
-ASSERT NOT (e IS_IN r);
-%ASSERT e IS_IN r2;
-ASSERT (r <= r2);
-ASSERT NOT ((3,3) IS_IN r2);
-
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback