log/smt2perr141.smt2:1:22: expected decimal constant at 'oops'