summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/complement3.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets/complement3.cvc')
-rw-r--r--test/regress/regress0/sets/complement3.cvc15
1 files changed, 0 insertions, 15 deletions
diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc
deleted file mode 100644
index 762d186ed..000000000
--- a/test/regress/regress0/sets/complement3.cvc
+++ /dev/null
@@ -1,15 +0,0 @@
-% EXPECT: sat
-OPTION "sets-ext";
-OPTION "logic" "ALL";
-Atom : TYPE;
-C32 : SET OF [Atom];
-C2 : SET OF [Atom];
-C4 : SET OF [Atom];
-ATOM_UNIV : SET OF [Atom];
-V1 : Atom;
-ASSERT C32 = (~C2) & (~C4);
-ASSERT TUPLE(V1) IS_IN ~(C32);
-ASSERT ATOM_UNIV = UNIVERSE :: SET OF [Atom];
-ASSERT TUPLE(V1) IS_IN ATOM_UNIV;
-ASSERT TUPLE(V1) IS_IN ~(C2);
-CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback