bench/check-ce/func_call6_mono.mlw

   1
   2 (* similar to func_call4.mlw but uses a let to declare z *)
   3
   4 use int.Int
   5
   6 type t = { mutable c : int }
   7
   8 let z = { c = any int }
   9
  10 val g (): unit
  11   writes { z.c }
  12   ensures { z.c > old z.c }
  13
  14 let f () =
  15   z.c <- 0;
  16   g ();
  17   assert { z.c = 1 }