bench/infer/iff.mlw

   1
   2
   3 use int.Int
   4
   5 val g (x:int) : bool
   6   ensures { (result = True) <-> (x >= 0) }
   7
   8 let f [@bddinfer] (x:int) : unit =
   9   let ref y = 0 in
  10   let z = g x in
  11   [@bddinfer:beforeif]
  12   if z then
  13      [@bddinfer:then] y <- x else
  14      [@bddinfer:else] y <- -x;
  15   [@bddinfer:afterif]
  16   assert { y >= 0 }