sig
  type t
  val empty : Wp.Passive.t
  val is_empty : Wp.Passive.t -> bool
  val union : Wp.Passive.t -> Wp.Passive.t -> Wp.Passive.t
  val bind :
    fresh:Wp.Lang.F.var ->
    bound:Wp.Lang.F.var -> Wp.Passive.t -> Wp.Passive.t
  val join : Wp.Lang.F.var -> Wp.Lang.F.var -> Wp.Passive.t -> Wp.Passive.t
  val conditions :
    Wp.Passive.t -> (Wp.Lang.F.var -> bool) -> Wp.Lang.F.pred list
  val apply : Wp.Passive.t -> Wp.Lang.F.pred -> Wp.Lang.F.pred
  type binding =
      Bind of Wp.Lang.F.var * Wp.Lang.F.var
    | Join of Wp.Lang.F.var * Wp.Lang.F.var
  val iter : (Wp.Passive.binding -> unit) -> Wp.Passive.t -> unit
  val pretty : Stdlib.Format.formatter -> Wp.Passive.t -> unit
end