From f70e887d931e8577124b685a2969b205cc95fc48 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 20 Oct 2021 14:21:17 +0200
Subject: [PATCH] [eacsl] Do not print predicate result when translating RTE

---
 src/plugins/e-acsl/src/code_generator/assert.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index 88973e67824..8be5d95be4b 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
-- 
GitLab