(assert ((_ zero_extend 2147483640)(_ bv255 8)))