diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle index 1eb2d8e53928a8a268ddd53941f83df69495e7da..c7e6e96a3709a00ddc91b887078f6b1ce3484f20 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle @@ -2,7 +2,7 @@ [kernel] Parsing bitwise.i (no preprocessing) [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 49 goals scheduled +[wp] 51 goals scheduled [wp] [Qed] Goal typed_band_ensures : Valid [wp] [Qed] Goal typed_band_ensures_band0 : Valid [wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid @@ -52,8 +52,10 @@ [wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_positive2_ok : Valid [wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_negative_ok : Valid [wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_negative2_ok : Valid -[wp] Proved goals: 49 / 49 - Qed: 46 +[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed_ok : Valid +[wp] [Qed] Goal typed_cast_uchar_check_bit_to_signed2_ok : Valid +[wp] Proved goals: 51 / 51 + Qed: 48 Alt-Ergo: 3 ------------------------------------------------------------ Functions WP Alt-Ergo Total Success @@ -67,5 +69,5 @@ band_bool 1 1 2 100% bxor_bool 1 1 2 100% lemma 7 - 7 100% - cast_uchar 12 - 12 100% + cast_uchar 14 - 14 100% ------------------------------------------------------------