bench/check-ce/recursive_model.mlw

   1 module Test
   2   use int.Int
   3
   4   type nat = Z | S nat
   5
   6   val global : nat
   7
   8   let test (i : int)
   9   = assert {
  10       let _p = (0, 0) in (* <- The tuple introduces polymorphism! *)
  11       global <> Z -> i = 0
  12     }
  13 end
  14
  15 (* adapted from https://gitlab.inria.fr/why3/why3/-/issues/578 *)