bench/infer/bool_ops.mlw

   1
   2
   3 use ref.Ref
   4 use int.Int
   5 use bool.Bool
   6
   7 val random_bool () : bool
   8
   9 val andb (x:bool) (y:bool) : bool
  10   ensures { result = True <-> x = True /\ y = True }
  11
  12 let f  [@bddinfer] [@infer] () : bool
  13  diverges
  14  =
  15     let x = ref True in
  16     let y = ref True in
  17     let z = ref True in
  18     let a = ref True in
  19     while !z do
  20       x := random_bool ();
  21       y := random_bool ();
  22       z := andb !x !y;
  23       a := !z;
  24     done;
  25     !a