diff --git a/src/plugins/wp/tests/wp_gallery/euclid.c b/src/plugins/wp/tests/wp_gallery/euclid.c
index 130896edb869eda985da946cc155712452c388bb..a2edb06407a9901a8107230618b343d4e38bddfd 100644
--- a/src/plugins/wp/tests/wp_gallery/euclid.c
+++ b/src/plugins/wp/tests/wp_gallery/euclid.c
@@ -29,6 +29,7 @@ int euclid_gcd(int a, int b)
int r;
/*@
loop assigns a, b, r;
+ loop invariant \abs(a) <= INT_MAX && \abs(b) <= INT_MAX ;
loop invariant gcd(a,b) == \at( gcd(a,b), Pre );
loop variant \abs(b);
*/
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 5de7d3a8e0a74e093ca04765c8370a920f6ec4ca..42c40f083cedc77c9bc1d92e6cb7212035a8aed2 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
@@ -4,7 +4,7 @@
[rte:annot] annotating function euclid_gcd
[wp] [Valid] Goal euclid_gcd_exits (Cfg) (Unreachable)
[wp] [Valid] Goal euclid_gcd_terminates (Cfg) (Trivial)
-[wp] 16 goals scheduled
+[wp] 19 goals scheduled
[wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
[wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
@@ -13,21 +13,24 @@
[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)
+[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_2_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_2_established (Qed)
[wp] [Valid] typed_euclid_euclid_gcd_assert_rte_division_by_zero (Qed)
[wp] [Valid] typed_euclid_euclid_gcd_assert_rte_signed_overflow (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_euclid_gcd_assert_rte_signed_overflow_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_assigns (Qed)
[wp] [Valid] typed_euclid_euclid_gcd_assigns_part1 (Qed)
[wp] [Valid] typed_euclid_euclid_gcd_assigns_part2 (Qed)
[wp] [Valid] typed_euclid_euclid_gcd_assigns_part3 (Qed)
[wp] [Valid] typed_euclid_euclid_gcd_loop_variant_decrease (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_variant_positive (Qed)
-[wp] Proved goals: 18 / 18
+[wp] Proved goals: 21 / 21
Terminating: 1
Unreachable: 1
- Qed: 7
- Alt-Ergo: 9
+ Qed: 8
+ Alt-Ergo: 11
Smoke Tests: 5 / 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- euclid_gcd 7 9 16 100%
+ euclid_gcd 8 11 19 100%
------------------------------------------------------------