sig
  type step = private {
    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
  and sequence
  type sequent = Conditions.sequence * Lang.F.pred
  val step :
    ?descr:string ->
    ?stmt:Cil_types.stmt ->
    ?deps:Property.t list ->
    ?warn:Warning.Set.t -> Conditions.condition -> Conditions.step
  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 seq_list : 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 iteri :
    ?from:int ->
    (int -> Conditions.step -> unit) -> Conditions.sequence -> unit
  val condition : Conditions.sequence -> Lang.F.pred
  val close : Conditions.sequent -> Lang.F.pred
  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 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 sequence : Conditions.bundle -> Conditions.sequence
  exception Contradiction
  class type simplifier =
    object
      method assume : Lang.F.pred -> unit
      method copy : Conditions.simplifier
      method fixpoint : unit
      method infer : Lang.F.pred list
      method name : string
      method simplify_branch : Lang.F.pred -> Lang.F.pred
      method simplify_goal : Lang.F.pred -> Lang.F.pred
      method simplify_hyp : Lang.F.pred -> Lang.F.pred
      method target : Lang.F.pred -> unit
    end
  val clean : Conditions.sequent -> Conditions.sequent
  val filter : Conditions.sequent -> Conditions.sequent
  val letify :
    ?solvers:Conditions.simplifier list ->
    Conditions.sequent -> Conditions.sequent
  val pruning :
    ?solvers:Conditions.simplifier list ->
    Conditions.sequent -> Conditions.sequent
end