summaryrefslogtreecommitdiff
path: root/test/regress/regress1/rels/set-strat.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/rels/set-strat.cvc')
-rw-r--r--test/regress/regress1/rels/set-strat.cvc24
1 files changed, 0 insertions, 24 deletions
diff --git a/test/regress/regress1/rels/set-strat.cvc b/test/regress/regress1/rels/set-strat.cvc
deleted file mode 100644
index c56a2b16e..000000000
--- a/test/regress/regress1/rels/set-strat.cvc
+++ /dev/null
@@ -1,24 +0,0 @@
-% EXPECT: sat
-OPTION "logic" "ALL";
-IntPair: TYPE = [ INT, INT];
-SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ];
-x : SET OF IntPair;
-y : SET OF IntPair;
-w : SET OF IntPair;
-z : SET OF SetIntPair;
-
-a : IntPair;
-b : IntPair;
-
-ASSERT NOT a = b;
-
-ASSERT a IS_IN x;
-ASSERT b IS_IN y;
-ASSERT b IS_IN w;
-ASSERT (x,y) IS_IN z;
-ASSERT (w,x) IS_IN z;
-ASSERT NOT ( (x,x) IS_IN (z JOIN z) );
-
-ASSERT (x, { ( 0, 0 ) } ) IS_IN (z JOIN z);
-
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback