summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/complement3.cvc
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-04-21 09:26:04 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-04-21 09:26:19 -0500
commita33dac29d9cc8520f62b6e4f4f9138ea4e3fbcd4 (patch)
treeb92bc3f34aca16a4b4ed6d42b2c2ae909dff17d4 /test/regress/regress0/sets/complement3.cvc
parent8a0d2b0577e174d2078026129dd01ea46f7f984a (diff)
Handle subtypes in sets. Bug fixes for tuples with subtypes.
Diffstat (limited to 'test/regress/regress0/sets/complement3.cvc')
-rw-r--r--test/regress/regress0/sets/complement3.cvc3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc
index ff527a9b3..fa0a31e40 100644
--- a/test/regress/regress0/sets/complement3.cvc
+++ b/test/regress/regress0/sets/complement3.cvc
@@ -1,4 +1,5 @@
% EXPECT: sat
+OPTION "sets-ext";
OPTION "logic" "ALL_SUPPORTED";
Atom : TYPE;
C32 : SET OF [Atom];
@@ -11,4 +12,4 @@ 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; \ No newline at end of file
+CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback