diff options
Diffstat (limited to 'test/regress/regress0/rels/prod-mod-eq.cvc')
-rw-r--r-- | test/regress/regress0/rels/prod-mod-eq.cvc | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/prod-mod-eq.cvc b/test/regress/regress0/rels/prod-mod-eq.cvc new file mode 100644 index 000000000..96ef2ffba --- /dev/null +++ b/test/regress/regress0/rels/prod-mod-eq.cvc @@ -0,0 +1,26 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntPairPair: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPairPair; +z1 : SET OF IntPair; +w1 : SET OF IntPair; +z2 : SET OF IntPair; +w2 : SET OF IntPair; + +%ASSERT NOT (0,1,2,3) IS_IN (x PRODUCT y); + +ASSERT NOT( z = (x PRODUCT y) ); + +ASSERT (0,1,2,3) IS_IN z; + +ASSERT (0,1) IS_IN z1; +ASSERT (0,1) IS_IN z2; +ASSERT (2,3) IS_IN w1; +ASSERT (2,3) IS_IN w2; + +ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 ); + +CHECKSAT; |