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

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

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