double_projection.mlw 313 Bytes
Newer Older
1 2 3 4 5 6 7 8

module Test

  use int.Int

  type t

  function d (x : t) : int
9

10 11 12
  meta "model_projection" function d

  function c (x : t) : int
13

14 15 16
  meta "model_projection" function c

(* Here the counterexample should not be a record *)
17
  let f (x: t) : (_t: t)
18
    requires { c x > 0 }
19
    ensures  { d x < 0 }
20 21 22
  =
    x
end