log/smt2perr149.smt2:1:9: undefined symbol 'undefined'