diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 8a01575729702dc47de5c17c51f41cf9f03c8f4f..573e3a58ea1bc1f871f4f2efedf8a975dc1fa5a3 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -176,18 +176,12 @@ let labels_assert_after ~kf s l_post = function
| BuiltinLabel Here as l -> option l l_post
| l -> labels_fct ~kf ~at:s l
-let labels_loop_inv ~established s = function
- | BuiltinLabel Here -> Clabels.here
+let labels_loop s = function
+ | BuiltinLabel (Here | LoopCurrent) -> Clabels.here
| BuiltinLabel LoopEntry -> Clabels.loop_entry s
- | BuiltinLabel LoopCurrent ->
- if established
- then Clabels.loop_entry s
- else Clabels.loop_current s
| FormalLabel wplabel -> Clabels.formal wplabel
| l -> labels_fct ?kf:None ?at:None l (* current loop is handled above *)
-let labels_loop_assigns s l = labels_loop_inv ~established:false s l
-
(* -------------------------------------------------------------------------- *)
(* --- User Defined Predicates --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index aa179c41644f6f36800e17a706218496fa4c482f..962cfeaef0a86ab027c628778968f307eb0a4de3 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -34,8 +34,7 @@ val labels_fct_post : label_mapping
val labels_fct_assigns : label_mapping
val labels_assert_before : kf:kernel_function -> stmt -> label_mapping
val labels_assert_after : kf:kernel_function -> stmt -> c_label option -> label_mapping
-val labels_loop_inv : established:bool -> stmt -> label_mapping
-val labels_loop_assigns : stmt -> label_mapping
+val labels_loop : stmt -> label_mapping
val labels_stmt_pre : kf:kernel_function -> stmt -> label_mapping
val labels_stmt_post : kf:kernel_function -> stmt -> c_label option -> label_mapping
val labels_stmt_assigns : kf:kernel_function -> stmt -> c_label option -> label_mapping
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
index 23bbba6733ff9920e819f21fcd5effcb81cd8422..81c0ed9a9db7f1fea76ada3447ea8325532e6c3f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
@@ -13,7 +13,8 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'A' (file tests/wp_bts/issue_801.i, line 11):
-Prove: true.
+Assume { Type: is_sint32(s). (* Then *) Have: s <= 9. }
+Prove: false.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/38ad37c131db641f57e3de6a0eaa1a2d.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/38ad37c131db641f57e3de6a0eaa1a2d.json
new file mode 100644
index 0000000000000000000000000000000000000000..16d19ceb388989d8142fd2c2a7248345ad165cd2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/38ad37c131db641f57e3de6a0eaa1a2d.json
@@ -0,0 +1 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
index 5da74e2177681040534ed999560a6b27cafa5773..e8a8fbf9f5182bb26f413020f6b7ad3e374a0c6d 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
@@ -5,15 +5,15 @@
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_LoopCurrent_ensures : Valid
-[wp] [Qed] Goal typed_LoopCurrent_loop_invariant_A_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_LoopCurrent_loop_invariant_A_preserved : Unsuccess
[wp] [Qed] Goal typed_LoopCurrent_loop_invariant_A_established : Valid
[wp] [Qed] Goal typed_LoopCurrent_loop_assigns : Valid
[wp] [Qed] Goal typed_LoopCurrent_loop_variant_decrease : Valid
[wp] [Alt-Ergo 2.0.0] Goal typed_LoopCurrent_loop_variant_positive : Valid
-[wp] Proved goals: 6 / 6
- Qed: 5
- Alt-Ergo 2.0.0: 1
+[wp] Proved goals: 5 / 6
+ Qed: 4
+ Alt-Ergo 2.0.0: 1 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- LoopCurrent 5 1 6 100%
+ LoopCurrent 4 1 6 83.3%
------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 3c4b166db900c8676bb09277b0e6b474cc28bfc6..217da38b0854d57b056292892e7e74180a7a5154 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -380,13 +380,13 @@ let add_prop_loop_inv ~established config acc kind s ca p =
let id = WpPropId.mk_loop_inv_id ~established config.kf s ca in
match kind_to_select config kind id with
| None -> acc
- | Some kind -> WpStrategy.add_prop_loop_inv acc kind s ~established id p
+ | Some kind -> WpStrategy.add_prop_loop_inv acc kind s id p
let add_prop_inv_fixpoint config acc kind s ca p =
let id = WpPropId.mk_inv_hyp_id config.kf s ca in
match kind_to_select config kind id with
| None -> acc
- | Some kind -> WpStrategy.add_prop_loop_inv acc kind s ~established:false id p
+ | Some kind -> WpStrategy.add_prop_loop_inv acc kind s id p
(*----------------------------------------------------------------------------*)
(* Add Assigns *)
@@ -397,7 +397,7 @@ let add_loop_assigns_goal config s (ca, assigns) acc =
None -> acc
| Some id ->
if goal_to_select config id then
- let labels = NormAtLabels.labels_loop_assigns s in
+ let labels = NormAtLabels.labels_loop s in
let assigns' = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_loop_assigns_desc s assigns' in
WpStrategy.add_assigns acc WpStrategy.Agoal id a_desc
@@ -792,7 +792,7 @@ let add_variant_annot config s ca var_exp loop_entry loop_back =
WpStrategy.mk_variant_properties config.kf s ca var_exp
in
let add_variant acc kind id p =
- WpStrategy.add_prop_loop_inv acc kind s ~established:false id p
+ WpStrategy.add_prop_loop_inv acc kind s id p
in
let add_hyp acc =
let acc = add_variant acc WpStrategy.Ahyp vdecr_id vdecr in
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index f87b744a61755072dfc906ed4e3e2cd282fb4c1e..af09f957b438dff77ff268fc00abb4b02c398b81 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -224,8 +224,8 @@ let add_prop_assert acc kind kf s ca p =
let p = normalize id labels p in
add_prop acc kind id p
-let add_prop_loop_inv acc kind s ~established id p =
- let labels = NormAtLabels.labels_loop_inv ~established s in
+let add_prop_loop_inv acc kind s id p =
+ let labels = NormAtLabels.labels_loop s in
let p = normalize id labels p in
add_prop acc kind id p
@@ -375,7 +375,7 @@ let add_loop_assigns_hyp acc kf s asgn_opt = match asgn_opt with
let asgn = WpPropId.mk_loop_any_assigns_info s in
add_assigns_any acc Ahyp asgn
| Some id ->
- let labels = NormAtLabels.labels_loop_assigns s in
+ let labels = NormAtLabels.labels_loop s in
let assigns' = NormAtLabels.preproc_assigns labels assigns in
let a_desc = WpPropId.mk_loop_assigns_desc s assigns' in
add_assigns acc Ahyp id a_desc
diff --git a/src/plugins/wp/wpStrategy.mli b/src/plugins/wp/wpStrategy.mli
index 92b56332f031f2bbe583ff5a468dc2c1bbafbff8..3ae3b03b0c07b824e98afd7877d4d1ff52771dee 100644
--- a/src/plugins/wp/wpStrategy.mli
+++ b/src/plugins/wp/wpStrategy.mli
@@ -125,7 +125,7 @@ val add_prop_assert : t_annots -> annot_kind ->
kernel_function -> stmt -> code_annotation -> predicate -> t_annots
val add_prop_loop_inv : t_annots -> annot_kind ->
- stmt -> established:bool -> WpPropId.prop_id -> predicate -> t_annots
+ stmt -> WpPropId.prop_id -> predicate -> t_annots
(** {3 Adding assigns properties} *)