diff options
Diffstat (limited to 'test/regress/regress1/rels/strat_0_1.cvc')
-rw-r--r-- | test/regress/regress1/rels/strat_0_1.cvc | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/strat_0_1.cvc b/test/regress/regress1/rels/strat_0_1.cvc new file mode 100644 index 000000000..b91ddbbe8 --- /dev/null +++ b/test/regress/regress1/rels/strat_0_1.cvc @@ -0,0 +1,24 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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; |