bench/infer/pbinfer2_simplified.mlw

   1
   2 use int.Int
   3 use ref.Ref
   4
   5 val to_true (ii : bool) : int
   6   ensures { if ii then result = 1 else result = 100 }
   7
   8 let pgmtest [@bddinfer] [@infer](x: bool) : unit = [@vc:divergent]
   9   let a = ref false in
  10   while true do
  11           let _ = to_true false in
  12           let _ = to_true x in
  13           a := x
  14         done