diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index 88973e678249dfb95f3978dcfff5d78f761dea2d..8be5d95be4be239351847fa5fe05151de1089ea0 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -89,8 +89,13 @@ let register_term ~loc kf env ?force t e adata =
   register ~loc kf env name ?force e adata
 
 let register_pred ~loc kf env ?force p e adata =
-  let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
-  register ~loc kf env name ?force e adata
+  if Env.annotation_kind env == Smart_stmt.RTE then
+    (* When translating RTE, we do not want to print the result of the predicate
+       because they should be the only predicate in an assertion clause. *)
+    adata, env
+  else
+    let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
+    register ~loc kf env name ?force e adata
 
 let kind_to_string loc k =
   Cil.mkString