sig
  type step = private {
    mutable id : int;
    size : int;
    vars : Lang.F.Vars.t;
    stmt : Cil_types.stmt option;
    descr : string option;
    deps : Property.t list;
    warn : Warning.Set.t;
    condition : Conditions.condition;
  }
  and condition =
      Type of Lang.F.pred
    | Have of Lang.F.pred
    | When of Lang.F.pred
    | Core of Lang.F.pred
    | Init of Lang.F.pred
    | Branch of Lang.F.pred * Conditions.sequence * Conditions.sequence
    | Either of Conditions.sequence list
    | State of Mstate.state
  and sequence
  type sequent = Conditions.sequence * Lang.F.pred
  val pretty :
    (Stdlib.Format.formatter -> Conditions.sequent -> unit) Stdlib.ref
  val step :
    ?descr:string ->
    ?stmt:Cil_types.stmt ->
    ?deps:Property.t list ->
    ?warn:Warning.Set.t -> Conditions.condition -> Conditions.step
  val update_cond :
    ?descr:string ->
    ?deps:Property.t list ->
    ?warn:Warning.Set.t ->
    Conditions.step -> Conditions.condition -> Conditions.step
  val is_true : Conditions.sequence -> bool
  val is_empty : Conditions.sequence -> bool
  val vars_hyp : Conditions.sequence -> Lang.F.Vars.t
  val vars_seq : Conditions.sequent -> Lang.F.Vars.t
  val empty : Conditions.sequence
  val trivial : Conditions.sequent
  val sequence : Conditions.step list -> Conditions.sequence
  val seq_branch :
    ?stmt:Cil_types.stmt ->
    Lang.F.pred ->
    Conditions.sequence -> Conditions.sequence -> Conditions.sequence
  val append :
    Conditions.sequence -> Conditions.sequence -> Conditions.sequence
  val concat : Conditions.sequence list -> Conditions.sequence
  val iter : (Conditions.step -> unit) -> Conditions.sequence -> unit
  val list : Conditions.sequence -> Conditions.step list
  val size : Conditions.sequence -> int
  val steps : Conditions.sequence -> int
  val index : Conditions.sequent -> unit
  val step_at : Conditions.sequence -> int -> Conditions.step
  val is_trivial : Conditions.sequent -> bool
  val map_condition :
    (Lang.F.pred -> Lang.F.pred) ->
    Conditions.condition -> Conditions.condition
  val map_step :
    (Lang.F.pred -> Lang.F.pred) -> Conditions.step -> Conditions.step
  val map_sequence :
    (Lang.F.pred -> Lang.F.pred) ->
    Conditions.sequence -> Conditions.sequence
  val map_sequent :
    (Lang.F.pred -> Lang.F.pred) -> Conditions.sequent -> Conditions.sequent
  val insert :
    ?at:int -> Conditions.step -> Conditions.sequent -> Conditions.sequent
  val replace :
    at:int -> Conditions.step -> Conditions.sequent -> Conditions.sequent
  val subst :
    (Lang.F.term -> Lang.F.term) -> Conditions.sequent -> Conditions.sequent
  val introduction : Conditions.sequent -> Conditions.sequent option
  val introduction_eq : Conditions.sequent -> Conditions.sequent
  val lemma : Lang.F.pred -> Conditions.sequent
  val head : Conditions.step -> Lang.F.pred
  val have : Conditions.step -> Lang.F.pred
  val condition : Conditions.sequence -> Lang.F.pred
  val close : Conditions.sequent -> Lang.F.pred
  val at_closure : (Conditions.sequent -> Conditions.sequent) -> unit
  type bundle
  type 'a attributed =
      ?descr:string ->
      ?stmt:Cil_types.stmt ->
      ?deps:Property.t list -> ?warn:Warning.Set.t -> 'a
  val nil : Conditions.bundle
  val occurs : Lang.F.var -> Conditions.bundle -> bool
  val intersect : Lang.F.pred -> Conditions.bundle -> bool
  val merge : Conditions.bundle list -> Conditions.bundle
  val domain : Lang.F.pred list -> Conditions.bundle -> Conditions.bundle
  val intros : Lang.F.pred list -> Conditions.bundle -> Conditions.bundle
  val state :
    ?descr:string ->
    ?stmt:Cil_types.stmt ->
    Mstate.state -> Conditions.bundle -> Conditions.bundle
  val assume :
    (?init:bool -> Lang.F.pred -> Conditions.bundle -> Conditions.bundle)
    Conditions.attributed
  val branch :
    (Lang.F.pred ->
     Conditions.bundle -> Conditions.bundle -> Conditions.bundle)
    Conditions.attributed
  val either :
    (Conditions.bundle list -> Conditions.bundle) Conditions.attributed
  val extract : Conditions.bundle -> Lang.F.pred list
  val bundle : Conditions.bundle -> Conditions.sequence
  val clean : Conditions.sequent -> Conditions.sequent
  val filter : Conditions.sequent -> Conditions.sequent
  val parasite : Conditions.sequent -> Conditions.sequent
  val simplify :
    ?solvers:Lang.simplifier list ->
    ?intros:int -> Conditions.sequent -> Conditions.sequent
  val pruning :
    ?solvers:Lang.simplifier list -> Conditions.sequent -> Conditions.sequent
end