diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
index dfb0a7c81390b9910d10e663af4cc1bdf6d8774a..da93d6b571bbbf103a94d4fd733264cb8a94e7cb 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_strategy.c (with preprocessing)
-[rte] annotating function bts0513
-[rte] annotating function bts0513_bis
+[rte:annot] annotating function bts0513
+[rte:annot] annotating function bts0513_bis
[wp] Running WP plugin...
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index 768556112b11b4547149a138b6bbc0825804aa50..98bcd99641039e586c9d25533d31f4c0c9f640af 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function function
+[rte:annot] annotating function function
[wp] 39 goals scheduled
[wp] [Alt-Ergo] Goal typed_function_ensures : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
index d076d76ed0ca7aae9c361b7cb65df1b03f11b9d5..2c656c6f82589428c5d92e8c4a8f3218879fc66a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing chunk_typing_usable.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function usable_axiom
-[rte] annotating function usable_lemma
+[rte:annot] annotating function usable_axiom
+[rte:annot] annotating function usable_lemma
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 3 goals scheduled
[wp] [Coq] Goal typed_lemma_provable_lemma : Saved script
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle
index 26cfc3ad34548c8ce6555176bdabbf970c5b71e0..2ac1dd590cfe6848231ee11330f3a8a46de291ef 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing gnu_zero_array.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[wp] Running WP plugin...
[wp] gnu_zero_array.i:14: Warning:
Cast with incompatible pointers types (source: sint8*) (target: S*)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
index 2e8a5bd7c03ad64457355e2bf3317d3a86a3c29d..7ce463d9349eea815c4d793dc147ec1b41d0b8bc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
@@ -1,12 +1,12 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function assigned_via_pointer
-[rte] annotating function assigns
-[rte] annotating function assigns_effect
-[rte] annotating function chunk_typing
-[rte] annotating function initialized_assigns
-[rte] annotating function uninitialized_assigns
+[rte:annot] annotating function assigned_via_pointer
+[rte:annot] annotating function assigns
+[rte:annot] annotating function assigns_effect
+[rte:annot] annotating function chunk_typing
+[rte:annot] annotating function initialized_assigns
+[rte:annot] annotating function uninitialized_assigns
[kernel:annot:missing-spec] opaque_struct.i:79: Warning:
Neither code nor specification for function use, generating default assigns from the prototype
[wp] 15 goals scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
index dbb98c6df14292b6b3f805888a739fec56d47ac8..ca40bafd86e9470752fe7e8a3d7857e471e39c67 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing bts779.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function f
+[rte:annot] annotating function f
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Valid
[wp] [Alt-Ergo] Goal typed_f_assert_rte_mem_access : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
index 5072e7c6182b7fce459e1727cd69ba7b7bb4f8b5..92f813ec7b9afb87519940378b18806dc1ea12ed 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing bts_1360.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function foo_correct
-[rte] annotating function foo_wrong
+[rte:annot] annotating function foo_correct
+[rte:annot] annotating function foo_wrong
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_foo_wrong_ensures : Valid
[wp] [Qed] Goal typed_foo_wrong_assert_rte_mem_access : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 8b3b8ce8f5b18a8b19ab37dd367fb7231c48f8bf..fda9d1592fcde0fd6bf80aa7a818d7c719d0c3e7 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte -wp-timeout 20 -warn-unsigned-overflow [...]
[kernel] Parsing binary-multiplication-without-overflow.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function BinaryMultiplication
+[rte:annot] annotating function BinaryMultiplication
[wp] 16 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_half : Valid
[wp] [Qed] Goal typed_lemma_size : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 374c185811eccbf13ab99836f863fcb6f43c8ccb..c1ba41635544f4f8d2771e4caff691fbc95638e7 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing binary-multiplication.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function BinaryMultiplication
+[rte:annot] annotating function BinaryMultiplication
[wp] 17 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax4_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ax5_ok : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
index f3c3ceeb9d3ee22c07392c0ef679727b0dc47798..b6e73bdde324ab5d2f6961c6773b1b4b80656deb 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing bsearch.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function binary_search
+[rte:annot] annotating function binary_search
[wp] 28 goals scheduled
[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_default_requires
[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_loop_s3
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
index da9813c2fb9daf073f0babb7e050055580c2d224..d3aaf8ea83ff392207675938102fb74ad56eccaa 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing euclid.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function euclid_gcd
+[rte:annot] annotating function euclid_gcd
[wp] 16 goals scheduled
[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_default_requires
[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
index 0760f8c1ed9a053d7dae27231140e001e240e7e1..6fc4641c2a918d26bae446e524b503705425f3df 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
@@ -54,9 +54,9 @@
iter_ptr 2 6 8 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function find
-[rte] annotating function find_ptr
-[rte] annotating function iter_ptr
+[rte:annot] annotating function find
+[rte:annot] annotating function find_ptr
+[rte:annot] annotating function iter_ptr
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_find_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_find_assert_rte_signed_overflow : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
index 4b982f51859e9264450636ff771075ff5d74795a..472bae3aac8525769125b58c733be5e59855b4e9 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
@@ -21,7 +21,7 @@
exo1 6 4 10 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function exo1
+[rte:annot] annotating function exo1
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_mem_access : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
index 83f9d8a5be5060dfa8c264411f2da764ffe9f6ac..9fb7098252504e09573928fbe1ffe9c1284fd622 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
@@ -33,7 +33,7 @@
max_subarray 12 10 22 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function max_subarray
+[rte:annot] annotating function max_subarray
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_max_subarray_assert_rte_mem_access : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index 46675ba6fcb4418714a63d1d5c559f395d7e3c7a..dfc94d8a3943ced736b0721f08a7b01c3b7c69c7 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -54,7 +54,7 @@
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
-[rte] annotating function equal_elements
+[rte:annot] annotating function equal_elements
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 8dfaabe1c3834bffe2458219be7a460bedbd26ad..4bf9ab318fb2b123882eaa5b3254c0e63fcf9f24 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -55,7 +55,7 @@
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
-[rte] annotating function equal_elements
+[rte:annot] annotating function equal_elements
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
index e2cf934a567dc28914fecb97236a1751f6fcb264..9ca1fbbad3e4eaf7c77acb2bd4fd7bed774c63e1 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
@@ -37,7 +37,7 @@
pair 16 10 26 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function pair
+[rte:annot] annotating function pair
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_pair_assert_rte_index_bound : Valid
[wp] [Qed] Goal typed_pair_assert_rte_index_bound_2 : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
index 8ec3a7f69f5cf0634c4cb9febbde67189426537a..d6ad1f485b30f88a8479ac41b4c90ac59985ab2a 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
@@ -67,9 +67,9 @@
main 5 2 7 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function main
-[rte] annotating function stringCompare
-[rte] annotating function stringLength
+[rte:annot] annotating function main
+[rte:annot] annotating function stringCompare
+[rte:annot] annotating function stringLength
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access_2 : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
index fb13236dbf626facd576c4934ec557d2b0285c38..b34ba7805c8a383c50e53f0ce20467d47b9a4f90 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
@@ -3,7 +3,7 @@
[kernel] Parsing working_dir/swap.c (with preprocessing)
[kernel] Parsing working_dir/swap2.h (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function swap
+[rte:annot] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_ensures_A : Valid
[wp] [Qed] Goal typed_swap_ensures_B : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
index 15ac0f70d86c802229aaf2fdac0953b775713f3f..f22342a088335ac45d7694c7767e8f5304a6906b 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[rte] annotating function swap
+[rte:annot] annotating function swap
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
swap 5 3 8 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
index 4378c5286a802774782011e5efcf035646661793..f002fd6fea324372319cd2b9c60bae3af26c3fdc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
@@ -1,9 +1,9 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing rte.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function job
-[rte] annotating function job2
-[rte] annotating function job3
+[rte:annot] annotating function job
+[rte:annot] annotating function job2
+[rte:annot] annotating function job3
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Unsuccess