sig
  type step = private {
    size : int;
    vars : Wp.Lang.F.Vars.t;
    stmt : Cil_types.stmt option;
    descr : string option;
    deps : Property.t list;
    warn : Wp.Warning.Set.t;
    condition : Wp.Conditions.condition;
  }
  and condition =
      Type of Wp.Lang.F.pred
    | Have of Wp.Lang.F.pred
    | When of Wp.Lang.F.pred
    | Core of Wp.Lang.F.pred
    | Init of Wp.Lang.F.pred
    | Branch of Wp.Lang.F.pred * Wp.Conditions.sequence *
        Wp.Conditions.sequence
    | Either of Wp.Conditions.sequence list
  and sequence
  type sequent = Wp.Conditions.sequence * Wp.Lang.F.pred
  val step :
    ?descr:string ->
    ?stmt:Cil_types.stmt ->
    ?deps:Property.t list ->
    ?warn:Wp.Warning.Set.t -> Wp.Conditions.condition -> Wp.Conditions.step
  val is_empty : Wp.Conditions.sequence -> bool
  val vars_hyp : Wp.Conditions.sequence -> Wp.Lang.F.Vars.t
  val vars_seq : Wp.Conditions.sequent -> Wp.Lang.F.Vars.t
  val empty : Wp.Conditions.sequence
  val seq_list : Wp.Conditions.step list -> Wp.Conditions.sequence
  val seq_branch :
    ?stmt:Cil_types.stmt ->
    Wp.Lang.F.pred ->
    Wp.Conditions.sequence ->
    Wp.Conditions.sequence -> Wp.Conditions.sequence
  val append :
    Wp.Conditions.sequence ->
    Wp.Conditions.sequence -> Wp.Conditions.sequence
  val concat : Wp.Conditions.sequence list -> Wp.Conditions.sequence
  val iter : (Wp.Conditions.step -> unit) -> Wp.Conditions.sequence -> unit
  val iteri :
    ?from:int ->
    (int -> Wp.Conditions.step -> unit) -> Wp.Conditions.sequence -> unit
  val condition : Wp.Conditions.sequence -> Wp.Lang.F.pred
  val close : Wp.Conditions.sequent -> Wp.Lang.F.pred
  type bundle
  type 'a attributed =
      ?descr:string ->
      ?stmt:Cil_types.stmt ->
      ?deps:Property.t list -> ?warn:Wp.Warning.Set.t -> 'a
  val nil : Wp.Conditions.bundle
  val occurs : Wp.Lang.F.var -> Wp.Conditions.bundle -> bool
  val intersect : Wp.Lang.F.pred -> Wp.Conditions.bundle -> bool
  val merge : Wp.Conditions.bundle list -> Wp.Conditions.bundle
  val domain :
    Wp.Lang.F.pred list -> Wp.Conditions.bundle -> Wp.Conditions.bundle
  val intros :
    Wp.Lang.F.pred list -> Wp.Conditions.bundle -> Wp.Conditions.bundle
  val assume :
    (?init:bool ->
     Wp.Lang.F.pred -> Wp.Conditions.bundle -> Wp.Conditions.bundle)
    Wp.Conditions.attributed
  val branch :
    (Wp.Lang.F.pred ->
     Wp.Conditions.bundle -> Wp.Conditions.bundle -> Wp.Conditions.bundle)
    Wp.Conditions.attributed
  val either :
    (Wp.Conditions.bundle list -> Wp.Conditions.bundle)
    Wp.Conditions.attributed
  val extract : Wp.Conditions.bundle -> Wp.Lang.F.pred list
  val sequence : Wp.Conditions.bundle -> Wp.Conditions.sequence
  exception Contradiction
  class type simplifier =
    object
      method assume : Wp.Lang.F.pred -> unit
      method copy : Wp.Conditions.simplifier
      method fixpoint : unit
      method infer : Wp.Lang.F.pred list
      method name : string
      method simplify_branch : Wp.Lang.F.pred -> Wp.Lang.F.pred
      method simplify_goal : Wp.Lang.F.pred -> Wp.Lang.F.pred
      method simplify_hyp : Wp.Lang.F.pred -> Wp.Lang.F.pred
      method target : Wp.Lang.F.pred -> unit
    end
  val clean : Wp.Conditions.sequent -> Wp.Conditions.sequent
  val filter : Wp.Conditions.sequent -> Wp.Conditions.sequent
  val letify :
    ?solvers:Wp.Conditions.simplifier list ->
    Wp.Conditions.sequent -> Wp.Conditions.sequent
  val pruning :
    ?solvers:Wp.Conditions.simplifier list ->
    Wp.Conditions.sequent -> Wp.Conditions.sequent
end