regress/parser/smt2perr026.smt2:1:14: expected symbol after 'declare-fun'