diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 5199e4e66877841833130e726765a884a73618c8..83f51025ce22159bd623830357532d32a9c7874f 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -664,7 +664,6 @@ let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
   in
   t1, lv, t2
 
-
 let compute_guards loc ~is_forall p bounded_vars hyps =
   try
     let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
diff --git a/src/plugins/e-acsl/src/code_generator/translate_ats.ml b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
index c8c3a4197caa9c5b40ed2b4bba1f74484dcb1a34..5ce9da77b6243bc1a971465643c800e1e3495497 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_ats.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_ats.ml
@@ -305,11 +305,24 @@ let pretranslate_to_exp_with_lscope ~loc ~lscope kf env pot =
   let term_to_exp = !term_to_exp_ref in
   let lscope_vars = Lscope.get_all lscope in
   let lscope_vars = List.rev lscope_vars in
+  let rec add_lscope_to_logic_env env = function
+    | [] -> env
+    | (Lvs_quantif(t1,_,x,_,t2)::lscope) ->
+      let logic_env = Env.Logic_env.get env in
+      let i = Interval.join
+          (Interval.get ~logic_env t1)
+          (Interval.get ~logic_env t2)
+      in
+      add_lscope_to_logic_env
+        (Env.Logic_env.add_let_quantif_binding env x i)
+        lscope
+    | _::_ -> env
+  in
+  let env = add_lscope_to_logic_env env lscope in
   let logic_env = Env.Logic_env.get env in
   let sizes_and_shifts =
     sizes_and_shifts_from_quantifs ~loc ~logic_env kf lscope_vars []
   in
-  let logic_env = Env.Logic_env.get env in
   (* Creating the pointer *)
   let ty = match pot with
     | PoT_pred _ ->