diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index abd2c08e061c483ab77afb401484158e7d825f51..bdd66e6ceacff29e6a49b27351ea8d2c1e790b3d 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,7 @@
 Plugin E-ACSL <next-release>
 ###############################################################################
 
+-* E-ACSL       [2024-09-16] fix logic variable escaping its scope
 -* E-ACSL       [2024-09-03] handle negative integers generated by RTE
 -* E-ACSL       [2024-08-30] fix typing exception occurring for applications
                 of axiomatically defined premises and logic functions
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 15fec0f05c3fc1784094848699d21790dfca44d8..e4f729209f8f92db3cdd65e46cf9c3ea7343d3dc 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -310,6 +310,7 @@ let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
   exp, env
 
 module Logic_binding = struct
+  let clear env = {env with var_mapping = Logic_var.Map.empty}
 
   let add_binding env logic_v vi =
     try
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 91d3aed298aabfff57f7403ded0cf06043a61f11..40569ada0a04036dc7461944bd4407fc92c2c67e 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -66,6 +66,8 @@ val rtl_call_to_new_var:
 *)
 
 module Logic_binding: sig
+  val clear : t -> t
+
   val add: ?ty:typ -> t -> kernel_function -> logic_var -> varinfo * exp * t
   (* Add a new C binding to the list of bindings for the logic variable. *)
 
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 0856f842134d8093f4f698c419dbd7e61d38088f..289cc2bb6f4e7fddee0a8e05350577e88c39165a 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -203,6 +203,9 @@ let generate_kf ~loc fname env params_ty ret_ty params_ival li =
      Delay its generation after filling the memoization table (for termination
      of recursive function calls) *)
   let gen_body () =
+    let env = (* cannot use bindings from other functions (the use site) *)
+      Env.Logic_binding.clear env
+    in
     let env = Env.push env in
     (* fill the typing environment with the function's parameters
        before generating the code (code generation invokes typing) *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index a2dcfd36b7b8c12fc540734a0ebad5fdf3739609..e898f1dca194d56a6739d4c4c149bffc153b5688 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -759,7 +759,8 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
   | Tapp(li, [], args)
   | Tapp(li, [BuiltinLabel Here], args) ->
     let e, adata, env =
-      Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args in
+      Logic_functions.app_to_exp ~adata ~loc ~tapp:t kf env li args
+    in
     let adata = Assert.register_term ~loc t e adata in
     e, adata, env, Analyses_types.C_number, "app"
   | Tapp(_, _ :: _, _) ->
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
index 60957b9d31adc346e4d9a2f21cdacdbc0fd1e31a..4bbf7e47df2d0ec31de4c9edc09c173f989977dd 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
@@ -53,8 +53,7 @@ int __gen_e_acsl_f(int x)
     long __gen_e_acsl_if_3;
     __gen_e_acsl_f_5 = __gen_e_acsl_f_2(0);
     __gen_e_acsl_v = __gen_e_acsl_f_5;
-    /*@ assert Eva: initialization: \initialized(&__gen_e_acsl_v_2); */
-    if (0L == __gen_e_acsl_v_2) __gen_e_acsl_if_3 = x - 1L;
+    if (0L == __gen_e_acsl_v) __gen_e_acsl_if_3 = x - 1L;
     else __gen_e_acsl_if_3 = 0L;
     __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
   }
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
index d3f26b8698b1c5b1a2ac507c861fa6f848ad8901..c8232575390299a96257003befe44109ebafb073 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
+++ b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
@@ -1,4 +1,3 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] let.c:12: Warning: 
-  accessing uninitialized left-value. assert \initialized(&__gen_e_acsl_v_2);
+[eva:alarm] let.c:17: Warning: assertion got status unknown.