
effect A : unit

let rec f ()
  (*@ requires (_^* ). A @*)
  (*@ ensures A @*)
=
  perform A


let middle ()
  (*@ requires (_^* ) @*)
  (*@ ensures A.A @*)
=
  perform A;
  match f () with
  | x -> x
  | effect A k -> continue k ()

let main 
  (*@ requires (_^* ) @*)
  (*@ ensures A.A @*)
= 
  match middle () with 
  | _ -> ()
  | effect A k -> continue k ()

@ requires (_^* ). A @
@ ensures A @
@ requires (_^* ) @
@ ensures A.A @
@ requires (_^* ) @
@ ensures A.A @

effect A : unit

let rec f ()
=
  perform A


let middle ()
=
  perform A;
  match f () with
  | x -> x
  | effect A k -> continue k ()

let main 
= 
  match middle () with 
  | _ -> ()
  | effect A k -> continue k ()
