diff --git a/src/plugins/e-acsl/src/analyses/lscope.ml b/src/plugins/e-acsl/src/analyses/lscope.ml
index 3f9c07423aeba2b0fa3fc4547c2cb908079f2fa0..3c6db344d7524c5687a20b99181e6eddbfc46a01 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.ml
+++ b/src/plugins/e-acsl/src/analyses/lscope.ml
@@ -33,6 +33,9 @@ let is_empty = function [] -> true | _ :: _ -> false
 
 let add lscope_var t = lscope_var :: t
 
+let remove lscope_var t =
+  List.filter (fun elt -> elt != lscope_var) t
+
 let get_all t = t
 
 let exists lv t =
diff --git a/src/plugins/e-acsl/src/analyses/lscope.mli b/src/plugins/e-acsl/src/analyses/lscope.mli
index e3a17b42b5256931fac5ff3bd27a4fac19aae8d0..3b3eba63e48cb8908c0b93e46a184c803ada9266 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.mli
+++ b/src/plugins/e-acsl/src/analyses/lscope.mli
@@ -39,6 +39,11 @@ val is_empty: t -> bool
 val add: lscope_var -> t -> t
 (* Return a new logic scope in which the given [lscope_var] has been added. *)
 
+val remove: lscope_var -> t -> t
+(** @return a new logic scope in which the given [lscope_var] has been removed
+    if it was present. Use physical equality to check if the [lscope_var] is
+    present. *)
+
 val get_all: t -> lscope_var list
 (* Return the list of [lscope_var] of the given logic scope.
    The first element is the last [lscope_var] that was added to [t], the
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 5abf328e72961c4558b0545b5f74945a704b8898..a0c70db9491df461646aebfd4ea4adb80900157d 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -375,6 +375,7 @@ end
 module Logic_scope = struct
   let get env = env.lscope
   let extend env lvs = { env with lscope = Lscope.add lvs env.lscope }
+  let remove env lvs = { env with lscope = Lscope.remove lvs env.lscope }
   let set_reset env bool = { env with lscope_reset = bool }
   let get_reset env = env.lscope_reset
   let reset env =
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 04117ede82a6491c523cc2544fee8d560d380493..7805d06efcbe286ba61395b913d3586fb98ff4f7 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -131,6 +131,10 @@ module Logic_scope: sig
   (** Add a new logic variable with its associated information in the
       logic scope of the environment. *)
 
+  val remove: t -> lscope_var -> t
+  (** Remove a logic variable and its associated information from the logic
+      scope of the environment. *)
+
   val reset: t -> t
   (** Return a new environment in which the logic scope is reset
       iff [set_reset _ true] has been called beforehand. Do nothing otherwise. *)
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 b9cc28a77ddf5cda057f7e64735a48074ed7a25c..d369220466f63974ff0d2ec2f2cac11508847858 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_predicates.ml
@@ -187,10 +187,15 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
            )
          env)
   | Plet(li, p) ->
+    (* Translate the term registered to the \let logic variable *)
+    let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+    (* Register the logic var to the logic scope *)
     let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
     let env = Env.Logic_scope.extend env lvs in
-    let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+    (* Translate the body of the \let *)
     let e, adata, env = to_exp ~adata kf env p in
+    (* Remove the logic var from the logic scope *)
+    let env = Env.Logic_scope.remove env lvs in
     Interval.Env.remove li.l_var_info;
     e, adata, env
   | Pforall _ | Pexists _ ->
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 c83b2e2ca8417a9e8a818a0828d9600df2984302..a1e55e5d0eb17749669e4a9642917b3f3e50c198 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -861,10 +861,15 @@ and context_insensitive_term_to_exp ~adata kf env t =
   | Tcomprehension _ -> Env.not_yet env "tset comprehension"
   | Trange _ -> Env.not_yet env "range"
   | Tlet(li, t) ->
+    (* Translate the term registered to the \let logic variable *)
+    let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+    (* Register the logic var to the logic scope *)
     let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
     let env = Env.Logic_scope.extend env lvs in
-    let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
+    (* Translate the body of the \let *)
     let e, adata, env = to_exp ~adata kf env t in
+    (* Remove the logic var from the logic scope *)
+    let env = Env.Logic_scope.remove env lvs in
     Interval.Env.remove li.l_var_info;
     e, adata, env, Typed_number.C_number, ""