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/let.c b/src/plugins/e-acsl/tests/constructs/let.c
new file mode 100644
index 0000000000000000000000000000000000000000..eef3a376cf152d0c7b4a8fad22dcdf0c5568cd11
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/let.c
@@ -0,0 +1,18 @@
+/* run.config
+   COMMENT: The same function is translated twice with different signatures.
+   COMMENT: This regression test ensures that translations of sub-terms do not
+   COMMENT: spill over from one translation to the other, falling out of scope.
+*/
+
+/*@
+
+logic ℤ f(ℤ x) =
+  x ≡ 0 ? 0 :
+    \let v = f(0);
+     0 ≡ v ? x - 1 : 0;
+
+*/
+
+int main() {
+  /*@ assert f(1) == 0; */
+}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
new file mode 100644
index 0000000000000000000000000000000000000000..4bbf7e47df2d0ec31de4c9edc09c173f989977dd
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
@@ -0,0 +1,84 @@
+/* Generated by Frama-C */
+#include "pthread.h"
+#include "sched.h"
+#include "signal.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "time.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@
+logic integer f(integer x) = x == 0? 0: (\let v = f(0); 0 == v? x - 1: 0);
+
+*/
+long __gen_e_acsl_f_2(int x);
+
+int __gen_e_acsl_f(int x);
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+  {
+    int __gen_e_acsl_f_6;
+    __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+    __gen_e_acsl_f_6 = __gen_e_acsl_f(1);
+    __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"f(1)",0,
+                                 __gen_e_acsl_f_6);
+    __gen_e_acsl_assert_data.blocking = 1;
+    __gen_e_acsl_assert_data.kind = "Assertion";
+    __gen_e_acsl_assert_data.pred_txt = "f(1) == 0";
+    __gen_e_acsl_assert_data.file = "let.c";
+    __gen_e_acsl_assert_data.fct = "main";
+    __gen_e_acsl_assert_data.line = 17;
+    __e_acsl_assert(__gen_e_acsl_f_6 == 0,& __gen_e_acsl_assert_data);
+    __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+  }
+  /*@ assert f(1) == 0; */ ;
+  __retres = 0;
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+/*@ assigns \result;
+    assigns \result \from x; */
+int __gen_e_acsl_f(int x)
+{
+  long __gen_e_acsl_if_4;
+  if (x == 0) __gen_e_acsl_if_4 = 0L;
+  else {
+    long __gen_e_acsl_v;
+    long __gen_e_acsl_f_5;
+    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;
+    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;
+  }
+  int __retres = (int)__gen_e_acsl_if_4;
+  return __retres;
+}
+
+/*@ assigns \result;
+    assigns \result \from x; */
+long __gen_e_acsl_f_2(int x)
+{
+  long __gen_e_acsl_if_2;
+  if (x == 0) __gen_e_acsl_if_2 = 0L;
+  else {
+    long __gen_e_acsl_v_2;
+    long __gen_e_acsl_f_4;
+    long __gen_e_acsl_if;
+    __gen_e_acsl_f_4 = __gen_e_acsl_f_2(0);
+    __gen_e_acsl_v_2 = __gen_e_acsl_f_4;
+    if (0L == __gen_e_acsl_v_2) __gen_e_acsl_if = x - 1L;
+    else __gen_e_acsl_if = 0L;
+    __gen_e_acsl_if_2 = __gen_e_acsl_if;
+  }
+  long __retres = (int)__gen_e_acsl_if_2;
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c8232575390299a96257003befe44109ebafb073
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
@@ -0,0 +1,3 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] let.c:17: Warning: assertion got status unknown.