Goal:
    G : t  HI : invariants  x : Z  le : 0 <= x  H : x < 0
  ============================
   (0 = x)


DEBUG:Going to execute:
zify_op