bench/check-ce/func_call1_mono.mlw

   1
   2 use int.Int
   3
   4 type t = { mutable c : int }
   5
   6 val z: t
   7
   8 let g (x: int)
   9   writes { z.c }
  10   ensures { z.c > old z.c }
  11   ensures { result = x + 1 }
  12 = z.c <- z.c + 1;
  13   x + 1
  14
  15 let f () =
  16   z.c <- 0;
  17   let w = g 2 + 3 in
  18   assert { z.c = 1 }