regress/parser/smt2perr195.smt2:3:64: undefined symbol 'm'