bench/check-ce/logic_function.mlw

   1
   2 use int.Int
   3
   4 function g (x:int) : int
   5
   6 let main_g (y:int) : unit
   7 =
   8   assert { g y <> 42 }
   9
  10 function h (x1:int) (x2:bool) : int
  11
  12 let main_h (y1:int) (y2:bool) : unit
  13 =
  14   assert { h y1 y2 <> 42 }
  15
  16 function f (x:int) : int
  17
  18 let main_f (y:int) : unit
  19   requires { y = 0 }
  20 =
  21   assert { f 0 <> y };
  22   assert { f 1 <> y }