diff options
Diffstat (limited to 'test/regress/regress0/sets/complement3.cvc')
| -rw-r--r-- | test/regress/regress0/sets/complement3.cvc | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc new file mode 100644 index 000000000..ff527a9b3 --- /dev/null +++ b/test/regress/regress0/sets/complement3.cvc @@ -0,0 +1,14 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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;
\ No newline at end of file |