diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 595dc566e1e836413c056e3c2c462ff3fedcf11a..6372c26f3f6fcae1a9b30f6b29a28102a7dd8a93 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -135,6 +135,20 @@ let generate_rte env =
   let local_env, _ = top env in
   local_env.rte
 
+let with_rte ~f env rte_value =
+  let old_rte_value = generate_rte env in
+  let env = rte env rte_value in
+  let env = f env in
+  let env = rte env old_rte_value in
+  env
+
+let with_rte_and_result ~f env rte_value =
+  let old_rte_value = generate_rte env in
+  let env = rte env rte_value in
+  let other, env = f env in
+  let env = rte env old_rte_value in
+  other, env
+
 (* ************************************************************************** *)
 
 (* eta-expansion required for typing generalisation *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index 3a5aebf2f5d4f1a0ea67af77099032535365f8e7..cb6633546cfaaa5527c2be9d5d7ce56e470c59f9 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -165,7 +165,26 @@ val pop_loop: t -> predicate list * t
 (* ************************************************************************** *)
 
 val rte: t -> bool -> t
+(** [rte env x] sets RTE generation to x for the given environment *)
+
 val generate_rte: t -> bool
+(** Returns the current value of RTE generation for the given environment *)
+
+val with_rte: f:(t -> t) -> t -> bool -> t
+(** [with_rte ~f env x] executes the given closure with RTE generation set to x,
+    and reset RTE generation to its original value afterwards.
+    This function does not handle exceptions at all. The user must handle them
+    either directly in the [f] closure or around the call to the function. *)
+
+val with_rte_and_result: f:(t -> 'a * t) -> t -> bool -> 'a * t
+(** [with_rte_and_result ~f env x] executes the given closure with RTE
+    generation set to x, and reset RTE generation to its original value
+    afterwards. [f] is a closure that takes an environment an returns a pair
+    where the first member is an arbitrary value and the second member is the
+    environment. The function will return the first member of the returned pair
+    of the closure along with the updated environment.
+    This function does not handle exceptions at all. The user must handle them
+    either directly in the [f] closure or around the call to the function. *)
 
 (* ************************************************************************** *)
 (** {2 Context for error handling} *)