regress/parser/smt2perr122.smt2:2:3: expected symbol