.code:
  PUSH 1
  NOT
  PUSH [tag0]
  JUMPI
  PUSH 13
  PUSH 128
  MSTORE
tag0: