diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index e413aea96d1290734789e73c693ed6cd09835a73..df114cc3a82e449378b97f09bed3b17ef872b5c1 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -707,7 +707,7 @@ let type_term ~use_gmp_opt ?ctx t =
     Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
   ignore (type_term ~use_gmp_opt ?ctx t)
 
-let type_named_predicate ?(must_clear=true) p =
+let type_named_predicate ~must_clear p =
   Options.feedback ~dkey ~level:3 "typing predicate '%a'."
     Printer.pp_predicate p;
   if must_clear then begin
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 7a7fd0f80d5df014274881863363855978cb820c..c35a8e81952ec3d5e12a25a553684e604b39665d 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -101,9 +101,12 @@ val type_term: use_gmp_opt:bool -> ?ctx:number_ty -> term -> unit
     [use_gmp_opt] is false, then the conversion to the given context is done
     even if -e-acsl-gmp-only is set. *)
 
-val type_named_predicate: ?must_clear:bool -> predicate -> unit
+val type_named_predicate: must_clear:bool -> predicate -> unit
 (** Compute the type of each term of the given predicate.
-    Set {!must_clear} to false in order to not reset the environment. *)
+
+    If {!must_clear} is true, the typing environment is reset before translating
+    the predicate. The environment should be reset when translating a new
+    assertion, and kept otherwise. *)
 
 val clear: unit -> unit
 (** Remove all the previously computed types. *)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 2b496a89f873c302cb7af4c9e2dfa24bc4da413c..f691e41ca97e75b885608e36c3f8e0340c5b163b 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -420,7 +420,7 @@ let call_with_tset ~loc ~arg_from_range ~arg_from_term ?(prepend_n_args=false) k
     in
     (* There's no more quantifiers in the arguments now, we can call back
        [prediate_to_exp] to translate the predicate as usual *)
-    Typing.type_named_predicate ~must_clear:true p_quantified;
+    Typing.type_named_predicate ~must_clear:false p_quantified;
     !predicate_to_exp_ref kf env p_quantified
   | [] ->
     (* No arguments require quantifiers, so we can directly translate the
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 860c165a18a755e192fafce556955d898fb41ea4..9ad2815d009281c1143843a02d583511f334e229 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1050,6 +1050,11 @@ and predicate_to_exp ?name kf ?rte env p =
     e
 
 and generalized_untyped_predicate_to_exp ?name kf ?rte ?must_clear_typing env p =
+  (* If [rte] is true, it means we're translating the root predicate of an
+     assertion and we need to generate the RTE for it. The typing environment
+     must be cleared. Otherwise, if [rte] is false, it means we're already
+     translating RTE predicates as part of the translation of another root
+     predicate, and the typing environment must be kept. *)
   let rte = match rte with None -> Env.generate_rte env | Some b -> b in
   let must_clear = match must_clear_typing with None -> rte | Some b -> b in
   Typing.type_named_predicate ~must_clear p;
diff --git a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
index 4cb9d45b44a903599da58cbd1453c3d143c6446c..7af22946ecf5b94fc25c67c1ef326e157878a2ef 100644
--- a/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
@@ -48,6 +48,9 @@ int main(void) {
   /*@ assert !\valid_read(&t3[6][1][0] + (2..10)); */
   /*@ assert \valid_read(&t3[(n-1)..(n+2)][1]); */
 
+  int t4[10][10][10];
+  /*@ assert \let x = 5; \valid(&t4[4][0..x][2]); */
+
   struct S s;
   s.a[0] = 7; s.a[1] = 8;
   /*@ assert \initialized(&s.a[0] + (1..1)); */ ;