type option = None | Some int

(* CE generation should not fail anymore because of
   eliminate_algebraic not losing attributes anymore *)

let f (a: option) : unit
  ensures {
    match a with
    | None -> 1=2
    | Some _a -> 3=3
    end
  }
  = ()
