bench/check-ce/func_call5_mono.mlw

   1
   2
   3 use int.Int
   4
   5 type t = { mutable c : int }
   6
   7 let g1 (y: int)
   8   requires { y > 0 }
   9   ensures { result.c >= y }
  10 = { c = y }
  11
  12 let f1 (x : int)
  13   requires { x > 0 }
  14 =
  15   let z = g1 x in
  16   assert { z.c = x }
  17
  18 let g2 (y: int) = { c = y + 1 }
  19
  20 let f2 (x: int) =
  21   let z = g2 x in
  22   assert { z.c = x }