log/smt2perr003.smt2:1:1: expected '(' at ')'