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 9ff53cc26317b5eaeb462585cd5fda4353588a58..ac921a318be08275381f558f6f55e0a47a049d54 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_2 : Valid
+[wp] [Alt-Ergo] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : 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 0eb42debb654a24e426ea4ecfbd56582aec9c09f..2ba23416456faa39cde87569f6ab9693ef9bc593 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_2 : Valid
+[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_2_requires_ok : 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 e3aa6c4c70ffb73ee23551dab4bb873fcd2d1de5..98ab24cc12de61c5d5ae89cbc5e7f47c915dc1c0 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_2 : Valid
+[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_2_requires : 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 aabf5e4e8e04fdf077fcf856d408c65ef0bf3d8c..03d5b7f2fd3a7dcd17af11e41b87908e51636da0 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_2 : Valid
+[wp] [Qed] Goal typed_f_call_g_2_requires : 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 5e751c422efeace96a90dcac31bcd5b4d4cdb41c..2a297e0ebefb2b37d8791372db2d79f4f853723e 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_2 : Valid
+[wp] [Alt-Ergo] Goal typed_caller_call_job_2_requires : 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_2 : Valid
+[wp] [Alt-Ergo] Goal typed_caller2_call_job2_2_requires : 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_2 : Valid
+[wp] [Alt-Ergo] Goal typed_caller3_call_job3_2_requires : 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 b00f33bc3a3cf726d602d2e1061d9b1208d9a6ba..894def5654e6c88349bb8a1f22669a3cf852d950 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -368,6 +368,17 @@ struct
let get_ip ip =
Uniquify1.unique_basename ip
+ (** Uniquify call-site for precondition check. So
+ that precondition of the same call-site are grouped *)
+ module CallSite = Datatype.Triple_with_collections
+ (Kernel_function)(Kernel_function)(Stmt)
+ (struct let module_name = "Wp.WpPropId.CallSite" end)
+ module Uniquify_Stmt = NameUniquify(CallSite)(struct
+ let name = "Wp.WpPropId.Names3."
+ let basename (caller_kf,callee_kf,_stmt) =
+ (Kernel_function.get_name caller_kf)^"_call_"^(Kernel_function.get_name callee_kf)
+ end)
+
let get_prop_id_base p =
match p.p_kind , p.p_prop with
| (PKTactic | PKCheck | PKProp | PKPropLoop) , p -> get_ip p
@@ -377,11 +388,20 @@ struct
| PKVarPos , p -> get_ip p ^ "_positive"
| PKAFctOut , p -> get_ip p ^ "_normal"
| PKAFctExit , p -> get_ip p ^ "_exit"
- | PKPre(_kf,stmt,pre) , _ ->
- let kf_name_of_stmt =
- Kernel_function.get_name
- (Kernel_function.find_englobing_kf stmt)
- in Printf.sprintf "%s_call_%s" kf_name_of_stmt (get_ip pre)
+ | PKPre(callee_kf,stmt,pre) , _ ->
+ let caller_kf = Kernel_function.find_englobing_kf stmt in
+ let call_string =
+ Uniquify_Stmt.unique_basename (caller_kf,callee_kf,stmt)
+ in
+ (** remove name of callee kernel function given by get_ip *)
+ let ip_string = get_ip pre in
+ let ip_string =
+ Extlib.opt_conv ip_string
+ (Extlib.string_del_prefix
+ ((Kernel_function.get_name callee_kf)^"_")
+ ip_string)
+ in
+ call_string^"_"^ip_string
let get_prop_id_basename p =
let basename = get_prop_id_base p in