diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle index 1673f54ff0726acb4d67b58f7851d6de1504ec6d..4b3a0044393faa02a60d3f95120b5a17991d3a11 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle @@ -4,7 +4,7 @@ [wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 17 goals scheduled -[wp] [Alt-Ergo] Goal typed_lemma_C_ko : Unsuccess +[wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess [wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess [wp] [Qed] Goal typed_caller_ensures_R : Valid [wp] [Alt-Ergo] Goal typed_caller_ensures_R1_ko : Unsuccess @@ -13,11 +13,11 @@ [wp] [Qed] Goal typed_caller_assigns_normal_part1 : Valid [wp] [Qed] Goal typed_caller_assigns_normal_part2 : Valid [wp] [Qed] Goal typed_caller_call_job_requires_A : Valid -[wp] [Qed] Goal typed_caller_call_job_requires_CA1 : Valid -[wp] [Alt-Ergo] Goal typed_caller_call_job_requires_CA2_ko : Unsuccess +[wp] [Qed] Goal typed_caller_call_job_check_requires_CA1 : Valid +[wp] [Alt-Ergo] Goal typed_caller_call_job_check_requires_CA2_ko : Unsuccess [wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid -[wp] [Alt-Ergo] Goal typed_job_ensures_CB1 : Valid -[wp] [Alt-Ergo] Goal typed_job_ensures_CB2_ko : Unsuccess +[wp] [Alt-Ergo] Goal typed_job_check_ensures_CB1 : Valid +[wp] [Alt-Ergo] Goal typed_job_check_ensures_CB2_ko : Unsuccess [wp] [Qed] Goal typed_job_assigns_exit : Valid [wp] [Qed] Goal typed_job_assigns_normal_part1 : Valid [wp] [Qed] Goal typed_job_assigns_normal_part2 : Valid