regress/parser/smt2perr205.smt2:6:7: undefined symbol 'x'