x: BITVECTOR(16);
ASSERT(x[15:15] = 0bin1);
ASSERT(x[15:1] = x[14:0]);
QUERY(x = 0bin1111111111111111);