diff --git a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml index 45c63bdac6afa9ea810d3f516d48822f54959a6e..c885230cc46982ff84f4f8b10026c54afff6859e 100644 --- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml +++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml @@ -327,17 +327,7 @@ and to_exp ~adata ?inplace ?name kf ?rte env p = in let env = if rte then !translate_rte_exp_ref kf env e else env in let env = Assert.do_pending_register_data env in - Extlib.nest - adata - (Typed_number.add_cast - ~loc:p.pred_loc - ?name - env - kf - None - Analyses_types.C_number - None - e) + (e, adata), env ) env)