sig
  val unreachable_proved : int Stdlib.ref
  val unreachable_failed : int Stdlib.ref
  val trivial_terminates : int Stdlib.ref
  val set_unreachable : WpPropId.prop_id -> unit
  val set_trivially_terminates : WpPropId.prop_id -> Property.Set.t -> unit
  type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
  val get_call_pre_strategies :
    model:WpContext.model -> Cil_types.stmt -> WpStrategy.strategy list
  val get_function_strategies :
    model:WpContext.model ->
    ?assigns:WpAnnot.asked_assigns ->
    ?bhv:string list ->
    ?prop:string list -> Kernel_function.t -> WpStrategy.strategy list
  val get_property_strategies :
    model:WpContext.model -> Property.t -> WpStrategy.strategy list
end