sig
  type step = private {
    mutable id : int;
    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
    | State of Wp.Mstate.state
  and sequence
  type sequent = Wp.Conditions.sequence * Wp.Lang.F.pred
  val pretty :
    (Format.formatter -> Wp.Conditions.sequent -> unit) Pervasives.ref
  val step :
    ?descr:string ->
    ?stmt:Cil_types.stmt ->
    ?deps:Property.t list ->
    ?warn:Wp.Warning.Set.t -> Wp.Conditions.condition -> Wp.Conditions.step
  val update_cond :
    ?descr:string ->
    ?deps:Property.t list ->
    ?warn:Wp.Warning.Set.t ->
    Wp.Conditions.step -> Wp.Conditions.condition -> Wp.Conditions.step
  val is_true : Wp.Conditions.sequence -> bool
  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 trivial : Wp.Conditions.sequent
  val sequence : 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 list : Wp.Conditions.sequence -> Wp.Conditions.step list
  val size : Wp.Conditions.sequence -> int
  val steps : Wp.Conditions.sequence -> int
  val index : Wp.Conditions.sequent -> unit
  val step_at : Wp.Conditions.sequence -> int -> Wp.Conditions.step
  val is_trivial : Wp.Conditions.sequent -> bool
  val map_condition :
    (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
    Wp.Conditions.condition -> Wp.Conditions.condition
  val map_step :
    (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
    Wp.Conditions.step -> Wp.Conditions.step
  val map_sequence :
    (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
    Wp.Conditions.sequence -> Wp.Conditions.sequence
  val map_sequent :
    (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
    Wp.Conditions.sequent -> Wp.Conditions.sequent
  val insert :
    ?at:int ->
    Wp.Conditions.step -> Wp.Conditions.sequent -> Wp.Conditions.sequent
  val replace :
    at:int ->
    Wp.Conditions.step -> Wp.Conditions.sequent -> Wp.Conditions.sequent
  val subst :
    (Wp.Lang.F.term -> Wp.Lang.F.term) ->
    Wp.Conditions.sequent -> Wp.Conditions.sequent
  val introduction : Wp.Conditions.sequent -> Wp.Conditions.sequent
  val lemma : Wp.Lang.F.pred -> Wp.Conditions.sequent
  val head : Wp.Conditions.step -> Wp.Lang.F.pred
  val have : Wp.Conditions.step -> Wp.Lang.F.pred
  val condition : Wp.Conditions.sequence -> Wp.Lang.F.pred
  val close : Wp.Conditions.sequent -> Wp.Lang.F.pred
  val at_closure : (Wp.Conditions.sequent -> Wp.Conditions.sequent) -> unit
  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 state :
    ?descr:string ->
    ?stmt:Cil_types.stmt ->
    Wp.Mstate.state -> 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 bundle : 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_exp : Wp.Lang.F.term -> Wp.Lang.F.term
      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 parasite : Wp.Conditions.sequent -> Wp.Conditions.sequent
  val simplify :
    ?solvers:Wp.Conditions.simplifier list ->
    ?intros:int -> Wp.Conditions.sequent -> Wp.Conditions.sequent
  val pruning :
    ?solvers:Wp.Conditions.simplifier list ->
    Wp.Conditions.sequent -> Wp.Conditions.sequent
end