log/smt2perr005.smt2:1:5: expected command at 'oops'