log/smt2perr138.smt2:1:9: expected '(' before '(_ extract'