diff --git a/src/plugins/wp/tests/wp_gallery/euclid.c b/src/plugins/wp/tests/wp_gallery/euclid.c
new file mode 100644
index 0000000000000000000000000000000000000000..257d8c9ba2f410dd70b61383e0ac790ff004a95a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/euclid.c
@@ -0,0 +1,41 @@
+/*
+  run.config
+  DONTRUN:
+ */
+
+/*
+  run.config_qualif
+  OPT: -wp-rte -wp-smoke-tests -wp-driver tests/wp_gallery/euclid.wp
+*/
+
+/*@
+  axiomatic Euclid {
+    logic integer gcd(integer a, integer b);
+  }
+*/
+
+
+#include <limits.h>
+
+/*@
+  requires \abs(a) <= INT_MAX ;
+  requires \abs(b) <= INT_MAX ;
+  assigns \nothing;
+  ensures \result == gcd(a,b);
+*/
+
+int euclid_gcd(int a, int b)
+{
+  int r;
+  /*@
+    loop assigns a, b, r;
+    loop invariant gcd(a,b) == \at( gcd(a,b), Pre );
+    loop variant \abs(b);
+  */
+  while( b != 0 ) {
+    r = b ;
+    b = a % b ;
+    a = r ;
+  }
+  return a < 0 ? -a : a;
+}
diff --git a/src/plugins/wp/tests/wp_gallery/euclid.wp b/src/plugins/wp/tests/wp_gallery/euclid.wp
new file mode 100644
index 0000000000000000000000000000000000000000..e25b8d00adbc95f33ac43cb04d82d136a94d11bc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/euclid.wp
@@ -0,0 +1,3 @@
+library Euclid:
+why3.import += "number.Gcd";
+logic integer gcd(integer, integer) = "Gcd.gcd" ;
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
new file mode 100644
index 0000000000000000000000000000000000000000..47d45d1b0ed709fdd1d5af2282f445826e0d115c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_gallery/euclid.c (with preprocessing)
+[wp] Running WP plugin...
+[rte] annotating function euclid_gcd
+[wp] 16 goals scheduled
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_default_requires
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_code_s6
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_code_s11
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_code_s12
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assert_rte_division_by_zero : Valid
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_loop_assigns : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assigns_part1 : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assigns_part2 : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assigns_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_loop_variant_positive : Valid
+[wp] Proved goals:   16 / 16
+  Qed:             7 
+  Alt-Ergo:        9
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  euclid_gcd                7        9       16       100%
+------------------------------------------------------------