log/smt2perr133.smt2:1:9: expected '(' before '(_ repeat'