(assert ((_ sign_extend 100000000000000000000000