sig
  val split :
    (WpPropId.prop_id -> '-> unit) -> WpPropId.prop_id -> 'Bag.t -> unit
  type proof
  val create_proof : WpPropId.prop_id -> WpAnnot.proof
  val add_proof :
    WpAnnot.proof -> WpPropId.prop_id -> Property.t list -> unit
  val is_composed : WpAnnot.proof -> bool
  val is_proved : WpAnnot.proof -> bool
  val target : WpAnnot.proof -> Property.t
  val dependencies : WpAnnot.proof -> Property.t list
  val missing_rte : Cil_types.kernel_function -> string list
  val filter_status : WpPropId.prop_id -> bool
  val get_called_preconditions_at :
    Cil_types.kernel_function -> Cil_types.stmt -> Property.t list
  val get_called_post_conditions :
    Cil_types.kernel_function -> Property.t list
  val get_called_exit_conditions :
    Cil_types.kernel_function -> Property.t list
  val get_called_assigns : Cil_types.kernel_function -> Property.t list
  type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
  val get_id_prop_strategies :
    ?assigns:WpAnnot.asked_assigns -> Property.t -> WpStrategy.strategy list
  val get_call_pre_strategies : Cil_types.stmt -> WpStrategy.strategy list
  val get_function_strategies :
    ?assigns:WpAnnot.asked_assigns ->
    ?bhv:string list ->
    ?prop:string list -> Kernel_function.t -> WpStrategy.strategy list
end