log/smt2perr116.smt2:1:10: resulting bit-width of 'repeat' too large