bench/check-ce/func_call3.mlw

   1
   2 use int.Int
   3
   4 val ref z: int
   5
   6 let g (x: int)
   7   writes { z }
   8   ensures { z > old z }
   9   returns { r -> r = x + 2 }
  10 = z <- z + 1;
  11   x + 1