sig
  val reset : unit -> unit
  val tapp_to_exp :
    loc:Cil_types.location ->
    string ->
    Env.t ->
    Cil_types.term ->
    Cil_types.logic_info ->
    Typing.number_ty list ->
    Cil_types.exp list -> Cil_types.varinfo * Cil_types.exp * Env.t
  val add_generated_functions :
    Cil_types.global list -> Cil_types.global list
  val named_predicate_to_exp_ref :
    (Cil_types.kernel_function ->
     Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
    Pervasives.ref
  val term_to_exp_ref :
    (Cil_types.kernel_function ->
     Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
    Pervasives.ref
end