log/smt2perr150.smt2:1:9: unexpected attribute ':undefined'