(assert ((_ repeat 65536)(_ bv1 32768))