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