log/smt2perr144.smt2:1:16: expected decimal constant at 'oopsy'