sig
  val must_translate : Property.t -> bool
  val must_translate_opt : Property.t option -> bool
  val gmp_to_sizet :
    adata:Assert.t ->
    loc:Cil_types.location ->
    name:string ->
    ?check_lower_bound:bool ->
    ?pp:Cil_types.term ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
  val comparison_to_exp :
    adata:Assert.t ->
    loc:Cil_types.location ->
    Cil_types.kernel_function ->
    Env.t ->
    Typing.number_ty ->
    ?e1:Cil_types.exp ->
    Cil_types.binop ->
    Cil_types.term ->
    Cil_types.term ->
    ?name:string -> Cil_types.term option -> Cil_types.exp * Assert.t * Env.t
  val conditional_to_exp :
    ?name:string ->
    loc:Cil_types.location ->
    Cil_types.kernel_function ->
    Cil_types.term option ->
    Cil_types.exp ->
    Cil_types.exp * Env.t -> Cil_types.exp * Env.t -> Cil_types.exp * Env.t
  val env_of_li :
    adata:Assert.t ->
    loc:Cil_types.location ->
    Cil_types.kernel_function ->
    Env.t -> Cil_types.logic_info -> Assert.t * Env.t
  val term_to_exp_ref :
    (adata:Assert.t ->
     Cil_types.kernel_function ->
     Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref
  val predicate_to_exp_ref :
    (adata:Assert.t ->
     ?name:string ->
     Cil_types.kernel_function ->
     ?rte:bool ->
     Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref
end