regress/parser/smt2perr051.smt2:1:38: missing ')'