regress/parser/smt2perr143.smt2:1:24: missing ')'