bench/infer/double_count_bool.mlw

   1 use bool.Bool
   2 use int.Int
   3
   4 val ref x : bool
   5 val ref y : bool
   6 val ref t0 : int
   7 val ref t1 : int
   8
   9 val randomb () : bool
  10
  11 let test [@bddinfer] ()
  12   diverges
  13   =
  14   t0 <- 0;
  15   t1 <- 0;
  16   x <- true;
  17   y <- False;
  18
  19   while true do
  20     invariant { y -> t0 + t1 >= 50 }
  21      x <- randomb();
  22      if x && (t0 <= 30) then
  23        t0 <- t0 + 1
  24      else
  25        if x && (t0 > 30) then
  26          t1 <- t1 + 1
  27        else
  28          (t0 <- 0; t1 <- 0);
  29     y <- (t1 >= 20);
  30   done