regress/parser/smt2perr015.smt2:1:14: missing ')'