(assert (= ((_ repeat 562949953421313)(_ bv1 32768)) (_ bv1 32768)))