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..60957b9d31adc346e4d9a2f21cdacdbc0fd1e31a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
@@ -0,0 +1,85 @@
+/* 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;
+    /*@ assert Eva: initialization: \initialized(&__gen_e_acsl_v_2); */
+    if (0L == __gen_e_acsl_v_2) __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..d3f26b8698b1c5b1a2ac507c861fa6f848ad8901
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
@@ -0,0 +1,4 @@
+[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);