x : BITVECTOR(32);

ASSERT(BVLT(x,0hex0000000a));
QUERY(BVLE(x,0hex00000000));