diff --git a/src/plugins/wp/tests/wp_bts/issue_825.i b/src/plugins/wp/tests/wp_bts/issue_825.i
new file mode 100644
index 0000000000000000000000000000000000000000..b4c514fccc8a01fa1619db4a0113f0f09d11b58d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_825.i
@@ -0,0 +1,16 @@
+/*@
+  ensures \false ;
+  assigns \nothing;
+*/
+void job(void)
+{
+  int i=0, K=0;
+  /*@
+    loop invariant \forall integer j; 0 < j < 0 ==> \false ;
+    loop assigns i ;
+  */
+  while (i < 10) {
+    K ++;
+    i ++;
+  }
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8bbd713c28ccb81b951260439fd875d98655edd2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
@@ -0,0 +1,40 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_825.i, line 2) in 'job':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (2/2):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..09e0f30d5ed76953ec9436802983bb9f4df69e53
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Qed] Goal typed_job_ensures : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job_assigns : Valid
+[wp] Proved goals:    6 / 6
+  Qed:             6
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job                       6        -        6       100%
+------------------------------------------------------------