bench/check-ce/func_call_mono.mlw

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