sig
  type tag =
      MARK of Cil_types.stmt
    | THEN of Cil_types.stmt
    | ELSE of Cil_types.stmt
    | CALL of Cil_types.stmt * Cil_types.kernel_function
    | CASE of Cil_types.stmt * int64 list
    | DEFAULT of Cil_types.stmt
    | ASSERT of Cil_types.identified_predicate * int * int
  val loc : Wp.Splitter.tag -> Cil_types.location
  val pretty : Format.formatter -> Wp.Splitter.tag -> unit
  val mark : Cil_types.stmt -> Wp.Splitter.tag
  val if_then : Cil_types.stmt -> Wp.Splitter.tag
  val if_else : Cil_types.stmt -> Wp.Splitter.tag
  val switch_cases : Cil_types.stmt -> int64 list -> Wp.Splitter.tag
  val switch_default : Cil_types.stmt -> Wp.Splitter.tag
  val cases :
    Cil_types.identified_predicate ->
    (Wp.Splitter.tag * Cil_types.predicate) list option
  val call : Cil_types.stmt -> Cil_types.kernel_function -> Wp.Splitter.tag
  type 'a t
  val empty : 'a Wp.Splitter.t
  val singleton : 'a -> 'a Wp.Splitter.t
  val group :
    Wp.Splitter.tag ->
    ('a list -> 'a) -> 'a Wp.Splitter.t -> 'a Wp.Splitter.t
  val union :
    ('a -> 'a -> 'a) ->
    'a Wp.Splitter.t -> 'a Wp.Splitter.t -> 'a Wp.Splitter.t
  val merge :
    left:('a -> 'c) ->
    both:('a -> 'b -> 'c) ->
    right:('b -> 'c) ->
    'a Wp.Splitter.t -> 'b Wp.Splitter.t -> 'c Wp.Splitter.t
  val merge_all :
    ('a list -> 'a) -> 'a Wp.Splitter.t list -> 'a Wp.Splitter.t
  val length : 'a Wp.Splitter.t -> int
  val map : ('a -> 'b) -> 'a Wp.Splitter.t -> 'b Wp.Splitter.t
  val iter : (Wp.Splitter.tag list -> 'a -> unit) -> 'a Wp.Splitter.t -> unit
  val fold :
    (Wp.Splitter.tag list -> 'a -> 'b -> 'b) -> 'a Wp.Splitter.t -> 'b -> 'b
  val exists : ('a -> bool) -> 'a Wp.Splitter.t -> bool
  val for_all : ('a -> bool) -> 'a Wp.Splitter.t -> bool
  val filter : ('a -> bool) -> 'a Wp.Splitter.t -> 'a Wp.Splitter.t
end