sig
  val predicate_to_exp :
    ?name:string ->
    Cil_types.kernel_function ->
    ?rte:bool -> Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t
  val generalized_untyped_predicate_to_exp :
    ?name:string ->
    Cil_types.kernel_function ->
    ?rte:bool ->
    ?must_clear_typing:bool ->
    Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t
  val translate_predicate :
    ?pred_to_print:Cil_types.predicate ->
    Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t
  val translate_rte_annots :
    (Stdlib.Format.formatter -> '-> unit) ->
    '->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.code_annotation list -> Env.t
  exception No_simple_term_translation of Cil_types.term
  exception No_simple_predicate_translation of Cil_types.predicate
  val untyped_term_to_exp :
    Cil_types.typ option -> Cil_types.term -> Cil_types.exp
  val untyped_predicate_to_exp : Cil_types.predicate -> Cil_types.exp
end