sig
val quantif_to_exp :
Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t
val predicate_to_exp_ref :
(adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
end