bench/check-ce/func_call5.mlw

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