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 : 'Wp.Splitter.t
  val singleton : '-> 'Wp.Splitter.t
  val group :
    Wp.Splitter.tag ->
    ('a list -> 'a) -> 'Wp.Splitter.t -> 'Wp.Splitter.t
  val union :
    ('-> '-> 'a) ->
    'Wp.Splitter.t -> 'Wp.Splitter.t -> 'Wp.Splitter.t
  val merge :
    left:('-> 'c) ->
    both:('-> '-> 'c) ->
    right:('-> 'c) ->
    'Wp.Splitter.t -> 'Wp.Splitter.t -> 'Wp.Splitter.t
  val merge_all :
    ('a list -> 'a) -> 'Wp.Splitter.t list -> 'Wp.Splitter.t
  val length : 'Wp.Splitter.t -> int
  val map : ('-> 'b) -> 'Wp.Splitter.t -> 'Wp.Splitter.t
  val iter : (Wp.Splitter.tag list -> '-> unit) -> 'Wp.Splitter.t -> unit
  val fold :
    (Wp.Splitter.tag list -> '-> '-> 'b) -> 'Wp.Splitter.t -> '-> 'b
  val exists : ('-> bool) -> 'Wp.Splitter.t -> bool
  val for_all : ('-> bool) -> 'Wp.Splitter.t -> bool
  val filter : ('-> bool) -> 'Wp.Splitter.t -> 'Wp.Splitter.t
end