sig
  type t
  val pretty : Format.formatter -> State_set.t -> unit
  val empty : State_set.t
  val singleton : Cvalue.Model.t * Trace.t -> State_set.t
  val of_list : (Cvalue.Model.t * Trace.t) list -> State_set.t
  val of_list_forget_history : Cvalue.Model.t list -> State_set.t
  val is_empty : State_set.t -> bool
  val length : State_set.t -> int
  val add : Cvalue.Model.t * Trace.t -> State_set.t -> State_set.t
  exception Unchanged
  val merge_into : State_set.t -> into:State_set.t -> State_set.t
  val merge : State_set.t -> State_set.t -> State_set.t
  val add_statement : State_set.t -> Cil_types.stmt -> State_set.t
  val fold :
    ('-> Cvalue.Model.t * Trace.t -> 'a) -> '-> State_set.t -> 'a
  val iter : (Cvalue.Model.t * Trace.t -> unit) -> State_set.t -> unit
  val exists : (Cvalue.Model.t -> bool) -> State_set.t -> bool
  val map :
    (Cvalue.Model.t * Trace.t -> Cvalue.Model.t * Trace.t) ->
    State_set.t -> State_set.t
  val reorder : State_set.t -> State_set.t
  val join : State_set.t -> Cvalue.Model.t * Trace.t
  val narrow : State_set.t -> State_set.t -> State_set.t
  val narrow_list : State_set.t list -> State_set.t
  val to_list : State_set.t -> Cvalue.Model.t list
end