(assert ((_ sign_extend 10000000000