bench/infer/val_call_unit_arg.mlw

   1 use int.Int
   2
   3 val ref x : int
   4 val ref y : int
   5
   6 val test () : unit
   7   writes { x, y }
   8   ensures { x + (old y) = 0 }
   9   ensures { y = (old x) }
  10
  11 let main [@bddinfer] () =
  12   x <- 42;
  13   y <- 37;
  14   test()