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

ASSERT (0bin0001000000000000 = BVPLUS(16, x, y));
CHECKSAT;
% EXPECT: sat