sig
  type bundle
  val dump : Format.formatter -> Conditions.bundle -> unit
  type 'a attributed =
      ?descr:string ->
      ?stmt:Cil_types.stmt ->
      ?deps:Property.t list -> ?warn:Warning.Set.t -> 'a
  val empty : 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
  type hypotheses
  val hypotheses : Conditions.bundle -> Conditions.hypotheses
  type sequent = Conditions.hypotheses * Lang.F.pred
  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
  val close : Conditions.sequent -> Lang.F.pred
  type linker
  type link = Lstmt of Cil_types.stmt | Lprop of Property.t
  val linker : unit -> Conditions.linker
  val get_link : Conditions.linker -> string -> Conditions.link
  val pretty :
    ?linker:Conditions.linker ->
    Format.formatter -> Conditions.sequent -> unit
end