diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index fee194ce70ab07b10bf6bdf595543c7b59b09f82..9ff53cc26317b5eaeb462585cd5fda4353588a58 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -13,7 +13,7 @@
[wp] [Qed] Goal typed_call_main_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_call_main_call_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
-[wp] [Alt-Ergo] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
+[wp] [Alt-Ergo] Goal typed_double_call_call_f_requires_qed_ok_Rf_2 : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_main_ensures_qed_ok_Emain : Valid
[wp] [Qed] Goal typed_main_call_f_requires_qed_ok_Rf : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
index ac5a52640069fe4f37d2173e5c5c77778a44fa53..0eb42debb654a24e426ea4ecfbd56582aec9c09f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle
@@ -17,7 +17,7 @@
[wp] [Qed] Goal typed_g_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_g_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_unreachable_smt_with_contract_ensures_ok_2 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid
+[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_requires_ok_2 : Valid
[wp] Proved goals: 8 / 8
Qed: 8
[wp] Report in: 'tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.0.report.json'
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index e18208021ccb21482035e39a7353f2c3dcf98688..e3aa6c4c70ffb73ee23551dab4bb873fcd2d1de5 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -65,7 +65,7 @@
[wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part5 : Valid
[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
-[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
+[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_ensures : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part2 : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
index 5bfd4b969d1181a464dfba7b4c2af80db87bcd2d..aabf5e4e8e04fdf077fcf856d408c65ef0bf3d8c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle
@@ -5,7 +5,7 @@
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_f_call_g_requires : Valid
-[wp] [Qed] Goal typed_f_call_g_requires : Valid
+[wp] [Qed] Goal typed_f_call_g_requires_2 : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_3 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
index 8676944fb53b5219663b759b05710eb35ea5ee66..5e751c422efeace96a90dcac31bcd5b4d4cdb41c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
@@ -8,19 +8,19 @@
[wp] [Alt-Ergo] Goal typed_caller_ensures_P1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_ensures_P2 : Valid
[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller_call_job_requires_2 : Valid
[wp] [Qed] Goal typed_caller2_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_R : Valid
[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires_2 : Valid
[wp] [Qed] Goal typed_caller3_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_R : Valid
[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires_2 : Valid
[wp] [Qed] Goal typed_job_ensures_K : Valid
[wp] [Qed] Goal typed_job_ensures_P : Valid
[wp] [Qed] Goal typed_job_assigns_part1 : Valid
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index da6d8ed1239dff5b40ae153185f6a32d79c35875..b00f33bc3a3cf726d602d2e1061d9b1208d9a6ba 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -383,7 +383,7 @@ struct
(Kernel_function.find_englobing_kf stmt)
in Printf.sprintf "%s_call_%s" kf_name_of_stmt (get_ip pre)
- let get_prop_id_name p =
+ let get_prop_id_basename p =
let basename = get_prop_id_base p in
match p.p_part with
| None -> basename
@@ -393,6 +393,14 @@ struct
if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
Printf.sprintf "%s_part%06d" basename (succ k)
+ module Uniquify2 = NameUniquify(PropId)(struct
+ let name = "Wp.WpPropId.Names2."
+ let basename = get_prop_id_basename
+ end)
+
+ let get_prop_id_name p =
+ Uniquify2.unique_basename p
+
end
(* -------------------------------------------------------------------------- *)