diff options
Diffstat (limited to 'test/regress/regress1/rels/bv1p-sat.cvc')
-rw-r--r-- | test/regress/regress1/rels/bv1p-sat.cvc | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress1/rels/bv1p-sat.cvc b/test/regress/regress1/rels/bv1p-sat.cvc deleted file mode 100644 index a48cb6407..000000000 --- a/test/regress/regress1/rels/bv1p-sat.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; -x : SET OF BvPair; -y : SET OF BvPair; - -a : BvPair; -b : BvPair; -c : BvPair; -d : BvPair; - -ASSERT DISTINCT ( a, b ); -ASSERT DISTINCT ( c, d ); - -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)); - - -CHECKSAT; |