diff options
Diffstat (limited to 'test/regress/regress1/rels/bv1p.cvc')
-rw-r--r-- | test/regress/regress1/rels/bv1p.cvc | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/bv1p.cvc b/test/regress/regress1/rels/bv1p.cvc new file mode 100644 index 000000000..130ccae97 --- /dev/null +++ b/test/regress/regress1/rels/bv1p.cvc @@ -0,0 +1,22 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; +x : SET OF BvPair; +y : SET OF BvPair; + +a : BvPair; +b : BvPair; +c : BvPair; +d : BvPair; +e : BvPair; + +ASSERT DISTINCT ( a, b ); +ASSERT DISTINCT ( c, d, e ); + +ASSERT a IS_IN x; +ASSERT b IS_IN x; +ASSERT a IS_IN y; +ASSERT b IS_IN y; +ASSERT (NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y)) AND NOT ( e IS_IN (x JOIN y)) ); + +CHECKSAT; |