summaryrefslogtreecommitdiff
path: root/test/regress/regress0/cvc3.userdoc.04.cvc
blob: 824690bcfa073d7796bc81524ac5970d38132fcc (plain) 
1
2
3
4
5
6
7
8
9

x, y, z, t, q : BITVECTOR(1024);

ASSERT x = ~x;
ASSERT x&y&t&z&q = x;
ASSERT x|y = t;
ASSERT BVXOR(x,~x) = t;

% EXPECT: valid
QUERY  FALSE;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback