summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/sizecheck.cvc
blob: e9326d9f6d9554a278881b265a92023ea628926a (plain) 
1
2
3
4
5
6
7

x : BITVECTOR(10);
y : BITVECTOR(12);

ASSERT (0bin0001000000000000 = BVPLUS(16, x, y));
CHECKSAT;
% EXPECT: sat
% EXIT: 10
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback