log/smt2perr147.smt2:1:12: invalid parametric term '_ oops'