sig
  type kind =
      K_Assert
    | K_Invariant
    | K_Variant
    | K_StmtSpec
    | K_Allocation
    | K_Assigns
    | K_Decreases
    | K_Terminates
    | K_Complete
    | K_Disjoint
    | K_Requires
    | K_Ensures
  val clear : unit -> unit
  val push : Kernel_function.t -> Keep_status.kind -> Property.t -> unit
  val before_translation : unit -> unit
  val must_translate : Kernel_function.t -> Keep_status.kind -> bool
end