diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index cd724a5c7eb91108b88090adbfc353f0d127dd2c..d1ac1c975021f38b650254140168081948f9a868 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -152,13 +152,13 @@ let results ~smoke prs =
else
let cached = List.fold_left
(fun c (_,r) -> if r.VCS.cached then succ c else c)
- 0 doomed in
+ 0 passed in
let stucked = List.map
(fun (p,r) -> p, ptime r.prover_time true)
- doomed in
+ passed in
let solver = List.fold_left
(fun t (_,r) -> t +. r.solver_time)
- 0.0 doomed in
+ 0.0 passed in
let provers = pmerge [Qed,ptime solver false] stucked in
let verdict =
if missing <> [] then NoResult else
@@ -166,7 +166,7 @@ let results ~smoke prs =
| [] -> NoResult
| u::w -> (snd @@ List.fold_left choose_worst u w).verdict in
let proved = List.length passed in
- let failed = List.length missing + List.length doomed in
+ let failed = List.length missing in
{ empty with verdict ; provers ; cached ; proved ; failed }
let add a b =
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index bdd6e296559d9c53f1ad7573ca2c57e4a9dece21..6eb4c7af7ce0544338e297d66d6202f9c8cd22cb 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -330,14 +330,14 @@ let do_wpo_success ~shell ~updating goal success =
else
let smoke = Wpo.is_smoke_test goal in
let stats = ProofEngine.consolidated goal in
+ let proof, target = Wpo.get_proof goal in
begin
- if shell || stats.verdict <> Valid then
+ if shell || proof <> `Passed then
do_report_stats ~shell ~updating goal ~smoke stats ;
- if smoke && stats.verdict <> Valid then
+ if smoke && proof <> `Passed then
begin
- let target = Wpo.get_target goal in
let source = fst (Property.location target) in
- Wp_parameters.warning ~source "Failed smoke-test"
+ Wp_parameters.warning ~once:true ~source "Failed smoke-test"
end ;
end
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
index 396c87807050b6e0e4616a17d21b39f5ef4e022c..483eeffddd0494f898f104a255ee845884a51554 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
@@ -6,17 +6,17 @@
[wp] [Valid] typed_globals_check_qed_ok (Qed)
[wp] [Valid] typed_globals_check_qed_ok_2 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_3 (Qed)
-[wp] [Unknown] typed_globals_check_qed_ko (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_4 (Qed)
-[wp] [Unknown] typed_globals_check_qed_ko_2 (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_5 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_6 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_7 (Qed)
[wp] [Valid] typed_globals_check_provable (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_2 (Alt-Ergo) (Cached)
-[wp] [Unknown] typed_globals_check_not_provable (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_not_provable (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_3 (Alt-Ergo) (Cached)
-[wp] [Unknown] typed_globals_check_qed_ko_3 (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko_3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_8 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_9 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_10 (Qed)
@@ -27,13 +27,13 @@
[wp] [Valid] typed_globals_check_provable_5 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_6 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_7 (Alt-Ergo) (Cached)
-[wp] [Unknown] typed_globals_check_qed_ko_4 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_qed_ko_5 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_qed_ko_6 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_qed_ko_7 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_not_provable_2 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_not_provable_3 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_not_provable_4 (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko_4 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_qed_ko_5 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_qed_ko_6 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_qed_ko_7 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_not_provable_2 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_not_provable_3 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_not_provable_4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_locals_check_qed_ok (Qed)
[wp] [Valid] typed_locals_check_qed_ok_2 (Qed)
[wp] [Valid] typed_locals_check_qed_ok_3 (Qed)
@@ -75,7 +75,7 @@
[wp] [Valid] typed_complex_struct_check_qed_ok_16 (Qed)
[wp] [Valid] typed_complex_struct_check_qed_ok_17 (Qed)
[wp] [Valid] typed_complex_struct_check_qed_ok_18 (Qed)
-[wp] [Valid] typed_complex_struct_check_provable (Script)
+[wp] [Valid] typed_complex_struct_check_provable (Script) (Qed 2/2)
[wp] Proved goals: 62 / 73
Qed: 52
Script: 1
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 03a05ff6f7358e9e056ac63b78c88dddb31715f6..810a70de3c6193f19f17bf3eb53be48442f6e952 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
@@ -19,7 +19,7 @@
[wp] [Valid] typed_BinaryMultiplication_loop_assigns (Qed)
[wp] [Valid] typed_BinaryMultiplication_loop_variant_decrease (Alt-Ergo) (Cached)
[wp] [Valid] typed_BinaryMultiplication_loop_variant_positive (Qed)
-[wp] [Valid] typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved (Script)
+[wp] [Valid] typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved (Script 4) (Qed 1/10) (Alt-Ergo 9/10) (Cached)
[wp] Proved goals: 17 / 17
Qed: 4
Script: 1
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 14a3c030932e5944cdf164f16da9c7dd1cb33b7f..8151ffdaf4fc436f8bb21ad5b60c1dba4ebbb82d 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
@@ -3,13 +3,13 @@
[wp] Running WP plugin...
[rte:annot] annotating function binary_search
[wp] 28 goals scheduled
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_loop_s3 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s17 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s18 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_loop_s3 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s17 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_binary_search_ensures_Result (Alt-Ergo) (Cached)
[wp] [Valid] typed_binary_search_ensures_Found (Qed)
[wp] [Valid] typed_binary_search_ensures_NotFound (Alt-Ergo) (Cached)
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 82d93e86a626a15a7b23ab031207a9199b48bbf6..41392f11994e8b9cadd1f3fbe446ec9d1914b2de 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
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[rte:annot] annotating function euclid_gcd
[wp] 16 goals scheduled
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_ensures (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_established (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
index 6840a8852096c9e2c0c1c24b2e72fa7cced4a925..dec011b76760a72643b0eaed7c6bce7c72b46035 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing bitmask0x8000.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
-[wp] [Valid] typed_lemma_res_n (Script)
-[wp] [Valid] typed_lemma_res_y (Script)
+[wp] [Valid] typed_lemma_res_n (Script) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
+[wp] [Valid] typed_lemma_res_y (Script) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
index 33b379e24f69cceaed99e8faa30611232b85bdc7..2dba4628c0184e5faec034f6cc2ff42abe907eba 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
@@ -3,13 +3,13 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_A_requires (Qed)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_A_requires (Qed)
[wp] doomed.i:27: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_B_requires (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_bar_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_B_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_bar_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Valid] typed_bar_ensures (Qed)
-[wp] [Passed (Invalid)] typed_buzz_wp_smoke_default_requires (Qed)
+[wp] [Failed (Doomed)] typed_buzz_wp_smoke_default_requires (Qed)
[wp] doomed.i:41: Warning: Failed smoke-test
[wp] [Valid] typed_buzz_ensures (Qed)
[wp] Proved goals: 5 / 7
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
index 114b97fe7dbdedeeb073eea3086a69c143a4739a..f42a17c0ef35833d84aae6a9963034b0e95c319e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:29: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:30: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:32: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
index 8876b4535d61df2d5fe645b73e255f0d5feb2e6d..5968d7b57854767ea0dabb1e4b1a92b16877c141 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
@@ -3,43 +3,42 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 33 goals scheduled
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_ensures (Qed)
[wp] [Valid] typed_f1_ok_exits (Qed)
-[wp] [Failed (Doomed)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_ensures (Qed)
[wp] [Valid] typed_f2_ok_exits (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] doomed_call.i:68: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
+[wp] [Failed (Doomed)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Valid] typed_f3_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_ensures (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Valid] typed_f4_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
-[wp] doomed_call.i:121: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
+[wp] [Passed (Unknown)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 28 / 33
Qed: 10 (failed: 5)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
index 4b8fcaef2ef1525f3aab216cc0679e450eb8d2ed..6d8460a9afbf5b18a351d87105721a621634227f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
@@ -3,46 +3,45 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_ensures_part1 (Qed)
[wp] [Valid] typed_f1_ok_ensures_part2 (Qed)
[wp] [Valid] typed_f1_ok_exits (Qed)
-[wp] [Failed (Doomed)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_ensures_part1 (Qed)
[wp] [Valid] typed_f2_ok_ensures_part2 (Qed)
[wp] [Valid] typed_f2_ok_exits_part1 (Qed)
[wp] [Valid] typed_f2_ok_exits_part2 (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] doomed_call.i:68: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
+[wp] [Failed (Doomed)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Valid] typed_f3_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_ensures (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Valid] typed_f4_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
-[wp] doomed_call.i:121: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
+[wp] [Passed (Unknown)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 31 / 36
Qed: 13 (failed: 5)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
index 4f879169d527ae78b7aa1aa6cf1feb727bd30d4e..b04f624016343814e80b66469328f7522275ce23 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
@@ -3,50 +3,50 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 46 goals scheduled
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_assigns_exit (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] doomed_dead.i:44: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ko_assigns_exit (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_assigns_exit (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_assert (Qed)
[wp] [Valid] typed_f4_ok_assigns_exit (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] doomed_dead.i:90: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ko_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
index 2440cab302ca1b6985b43a32c596825d7a57725c..09fda7dac2829b41c6718b8263bdc181f2ca9ceb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
@@ -3,52 +3,52 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 48 goals scheduled
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part3 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_assigns_exit (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part3 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] doomed_dead.i:44: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ko_assigns_exit (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_assigns_exit (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_assert (Qed)
[wp] [Valid] typed_f4_ok_assigns_exit (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] doomed_dead.i:90: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ko_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
index 2556b38935cac7951ff3003334970aa15eeace76..057f17ce24307b606735b56b63df5cec0f91452c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
@@ -3,8 +3,8 @@
[wp] Running WP plugin...
[rte:annot] annotating function access
[wp] 4 goals scheduled
-[wp] [Failed (Doomed)] typed_access_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_access_wp_smoke_dead_code_s5 (Qed)
+[wp] [Passed (Unknown)] typed_access_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_access_wp_smoke_dead_code_s5 (Qed)
[wp] doomed_localinit.i:11: Warning: Failed smoke-test
[wp] [Timeout] typed_access_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [Timeout] typed_access_assert_rte_mem_access_2 (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
index 0cecf94944c951f59fc11738330f7ef17f591553..bd83f9550eb97e037e26e36d2b22f647d5d97af3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Qed)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Qed)
[wp] doomed_loop.i:22: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Qed)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Qed)
[wp] doomed_loop.i:23: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Qed)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Qed)
[wp] doomed_loop.i:25: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Qed)
[wp] [Unknown] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
index 1f8c56608948e8a2c058176c0dc5b6f06384b215..d568292aa0e9a7480c4a0205d368723905f3c015 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
@@ -3,27 +3,26 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
-[wp] [Passed (Invalid)] typed_requires_wp_smoke_default_requires (Qed)
+[wp] [Failed (Doomed)] typed_requires_wp_smoke_default_requires (Qed)
[wp] doomed_pre.i:10: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:16: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_2_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_2_2_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_2_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_2_2_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:23: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_1_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_1_2_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_1_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_1_2_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:30: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_combined_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_combined_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Unknown)] typed_reqs_combined_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_combined_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:37: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_bhv_requires_assumes_wp_smoke_B_requires (Qed)
+[wp] [Failed (Doomed)] typed_bhv_requires_assumes_wp_smoke_B_requires (Qed)
[wp] doomed_pre.i:48: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_massumes_wp_smoke_B1_assumes (Qed)
-[wp] doomed_pre.i:56: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_reqs_massumes_wp_smoke_B2_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_massumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_B1_assumes (Qed)
[wp] doomed_pre.i:56: Warning: Failed smoke-test
+[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_B2_assumes (Qed)
[wp] Proved goals: 5 / 13
Qed: 0 (failed: 8)
Alt-Ergo: 5
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
index c8694f081d628e1a7e52c04f80fb61b96f397414..4b67d9a83d0e8d0216943f63a0e418cbbf205be8 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:30: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
index 1a708a992add7c82d300963eac233cc224019dcb..10bb9690dc0015fe08c334fdd38d203b07a7506f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
@@ -3,9 +3,9 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_B_preserved (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
index 3264f7d6554ff164fb3ec60fb9bcf0b116f222f9..f08449c571341bde111d32389402dfedb990dff4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
@@ -6,9 +6,9 @@
[wp] doomed_unreach.i:22: Warning: Failed smoke-test
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
-[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s5 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_job_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_job_wp_smoke_dead_code_s5 (Alt-Ergo) (Cached)
+[wp] [Passed (Stepout)] typed_job_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
[wp] [Valid] typed_job_assigns_part1 (Qed)
[wp] [Valid] typed_job_assigns_part2 (Qed)
[wp] [Valid] typed_job_assigns_part3 (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
index 44f4519c1fc5ce64b2adf663b730d845f546e5c7..7b37e132c51b4aad6e5d2bf25809da4e7f41ca78 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
@@ -5,9 +5,9 @@
[wp] doomed_unroll.i:15: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 5 goals scheduled
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s27 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_foo_wp_smoke_dead_code_s27 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_foo_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_foo_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_preserved (Qed)
[wp] [Valid] typed_foo_loop_invariant_established (Qed)
[wp] Proved goals: 5 / 5
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
index 03e42c0b78e8ec522699f41ee9945419d0170c09..1d90715d28d093556930a65d290b4b4b0659a721 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] unroll.i:21: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
-[wp] [Valid] typed_unrolled_loop_ensures_zero (Script)
+[wp] [Valid] typed_unrolled_loop_ensures_zero (Script 2) (Qed 18/18)
[wp] Proved goals: 1 / 1
Qed: 0
Script: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index def71a156f5561e74f8379e3f31adc22a1b0f1b8..4418f56a90d85bf66481ebe6bd70420009b3d67c 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -105,7 +105,6 @@
Prove: P_S(42).
------------------------------------------------------------
-[wp] [Unknown] typed_clear_in_step_check (Script)
[wp:script:allgoals]
typed_clear_ensures subgoal:
@@ -143,5 +142,4 @@
Prove: P_S(a + b).
------------------------------------------------------------
-[wp] [Unknown] typed_clear_ensures (Script)
[wp] Proved goals: 0 / 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
index d56e54307acb3e020712988d2d98dc8fa206acab..544ecdb40411be8f49d2be5b6b45e05414608408 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
@@ -54,7 +54,6 @@
Prove: false.
------------------------------------------------------------
-[wp] [Unknown] typed_function_loop_invariant_X_preserved (Script)
[wp:script:allgoals]
typed_function_loop_invariant_X_preserved subgoal:
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
index 7db5771084a2153d55e8fa9b7fa0289e8f7615a2..9730b99da4113fca895f5e07225f72831af86a92 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -14,7 +14,6 @@
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Script)
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
@@ -56,7 +55,4 @@
Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_u (Script)
-[wp] Proved goals: 2 / 2
- Qed: 0
- Script: 2
+[wp] Proved goals: 0 / 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
index 7db5771084a2153d55e8fa9b7fa0289e8f7615a2..9730b99da4113fca895f5e07225f72831af86a92 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -14,7 +14,6 @@
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Script)
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
@@ -56,7 +55,4 @@
Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_u (Script)
-[wp] Proved goals: 2 / 2
- Qed: 0
- Script: 2
+[wp] Proved goals: 0 / 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 9d27fa468795f483be98de6f81cbcbd7e2c2f53d..6fb2156c63fb2ea6a3e82f8a0034aee8d8f9a428 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -201,7 +201,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_branch_ensures (Script)
[wp:script:allgoals]
typed_test_step_branch_ensures subgoal:
@@ -224,7 +223,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_or_ensures (Script)
[wp:script:allgoals]
typed_test_step_or_ensures subgoal:
@@ -256,7 +254,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_and_ensures (Script)
[wp:script:allgoals]
typed_test_step_peq_ensures subgoal:
@@ -265,7 +262,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_peq_ensures (Script)
[wp:script:allgoals]
typed_test_step_peq_ensures subgoal:
@@ -282,7 +278,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_pneq_ensures (Script)
[wp:script:allgoals]
typed_test_step_pneq_ensures subgoal:
@@ -299,7 +294,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_neq_ensures (Script)
+[wp] [Unknown] typed_test_step_neq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_neq_ensures subgoal:
@@ -324,7 +319,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_leq_ensures (Script)
+[wp] [Unknown] typed_test_step_leq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_leq_ensures subgoal:
@@ -354,7 +349,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_lt_ensures (Script)
+[wp] [Unknown] typed_test_step_lt_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_lt_ensures subgoal:
@@ -379,7 +374,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_if_ensures (Script)
[wp:script:allgoals]
typed_test_step_if_ensures subgoal:
@@ -405,7 +399,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_fa_if_ensures (Script)
[wp:script:allgoals]
typed_test_step_fa_if_ensures subgoal:
@@ -427,7 +420,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_fa_or_ensures (Script)
[wp:script:allgoals]
typed_test_step_fa_or_ensures subgoal:
@@ -448,7 +440,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_fa_and_ensures (Script)
[wp:script:allgoals]
typed_test_inside_leq_ensures subgoal:
@@ -463,7 +454,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unknown] typed_test_inside_leq_ensures (Script)
+[wp] [Unknown] typed_test_inside_leq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_inside_leq_ensures subgoal:
@@ -494,7 +485,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unknown] typed_test_inside_lt_ensures (Script)
+[wp] [Unknown] typed_test_inside_lt_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_inside_lt_ensures subgoal:
@@ -525,7 +516,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unknown] typed_test_inside_neq_ensures (Script)
+[wp] [Unknown] typed_test_inside_neq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_inside_neq_ensures subgoal:
@@ -556,7 +547,6 @@
Prove: P_P.
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_and_ensures (Script)
[wp:script:allgoals]
typed_test_goal_and_ensures subgoal:
@@ -581,7 +571,6 @@
Prove: (L_LP=true).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_eq_ensures (Script)
[wp:script:allgoals]
typed_test_goal_eq_ensures subgoal:
@@ -598,7 +587,6 @@
Prove: (L_LP=false).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_neq_ensures (Script)
[wp:script:allgoals]
typed_test_goal_neq_ensures subgoal:
@@ -620,7 +608,6 @@
Prove: P_P.
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_if_ensures (Script)
[wp:script:allgoals]
typed_test_goal_if_ensures subgoal:
@@ -642,7 +629,6 @@
Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_and_ensures (Script)
[wp:script:allgoals]
typed_test_goal_ex_and_ensures subgoal:
@@ -659,7 +645,6 @@
Prove: P_P \/ P_Q \/ (exists i : Z. P_Pi(i)) \/ (exists i : Z. P_Qi(i)).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_or_ensures (Script)
[wp:script:allgoals]
typed_test_goal_ex_if_ensures subgoal:
@@ -674,7 +659,6 @@
Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_if_ensures (Script)
[wp:script:allgoals]
typed_test_goal_ex_if_ensures subgoal:
@@ -702,5 +686,4 @@
Prove: exists i : Z. P_Qi(i).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_imply_ensures (Script)
[wp] Proved goals: 0 / 23
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
index 4d3c4e24423d9b1510f3ddab3f9beb135dc7c1d2..efa47216f89c476a13e229ebd31226ffc773e3b9 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing induction.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Valid] typed_lemma_ByInd (Script)
+[wp] [Valid] typed_lemma_ByInd (Script) (Alt-Ergo 3/3) (Cached)
[wp] Proved goals: 1 / 1
Qed: 0
Script: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
index 7cd2f2e12457ff9e67975ac67d5025e303c87903..e85db6d3a63c0b305740199a22eed6c9f4b600f2 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing overflow.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
-[wp] [Valid] typed_lemma_j_incr_char (Script)
-[wp] [Valid] typed_lemma_j_incr_short (Script)
+[wp] [Valid] typed_lemma_j_incr_char (Script) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
+[wp] [Valid] typed_lemma_j_incr_short (Script) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
index a515c1fc7f8e0462c3232646c8c13dacabb09be3..7d03fba0ca5b9e06437c10b36a5b535f0befbb26 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
@@ -2,9 +2,9 @@
[kernel] Parsing unroll.i (no preprocessing)
[wp] Running WP plugin...
[wp] 3 goals scheduled
-[wp] [Valid] typed_lemma_LEFT (Script)
-[wp] [Valid] typed_lemma_RIGHT (Script)
-[wp] [Valid] typed_lemma_SUM (Script)
+[wp] [Valid] typed_lemma_LEFT (Script) (Qed 2/2)
+[wp] [Valid] typed_lemma_RIGHT (Script) (Qed 2/2)
+[wp] [Valid] typed_lemma_SUM (Script) (Qed 2/2)
[wp] Proved goals: 3 / 3
Qed: 0
Script: 3
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index e67a634d8b1d1af8828a2f5cb1cea7aca86bb5c0..4b470149e633d7c719500de32bf4c13f06b7ea39 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -4,28 +4,28 @@
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
[wp] [Valid] typed_init_t2_v2_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_part2 (Script)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_part3 (Script)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part1 (Qed)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part2 (Script)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part3 (Script)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v2_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v2_assigns_part2 (Script)
+[wp] [Valid] typed_init_t2_v2_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v3_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v3_loop_assigns_part2 (Script)
-[wp] [Valid] typed_init_t2_v3_loop_assigns_part3 (Script)
+[wp] [Valid] typed_init_t2_v3_loop_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_v3_loop_assigns_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v3_loop_assigns_2_part1 (Qed)
[wp] [Valid] typed_init_t2_v3_loop_assigns_2_part2 (Qed)
[wp] [Valid] typed_init_t2_v3_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v3_assigns_part2 (Script)
+[wp] [Valid] typed_init_t2_v3_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part2 (Script)
-[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part3 (Script)
+[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Script)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part3 (Qed)
[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Script)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] Proved goals: 23 / 23
Qed: 11
Script: 12