(assert (ite true (_ bv0 16) (_ bv0 15))