sig
  type t
  val pretty : Format.formatter -> Trace.t -> unit
  val bottom : Trace.t
  val top : Trace.t
  val join : Trace.t -> Trace.t -> Trace.t
  val initial : Cil_types.kernel_function -> Trace.t
  val add_disjunction :
    Property.t -> Cil_types.predicate Cil_types.named -> Trace.t -> Trace.t
  val add_statement : Cil_types.stmt -> Trace.t -> Trace.t
  val set_compute_trace : bool -> unit
end