regress/parser/smt2perr013.smt2:1:17: missing ')'