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