log/smt2perr130.smt2:1:14: expected '(' before '_'