diff --git a/src/plugins/wp/tests/wp_bts/issue_801.i b/src/plugins/wp/tests/wp_bts/issue_801.i
new file mode 100644
index 0000000000000000000000000000000000000000..8325393b05db613750bf3fd56eb3d3bb13783494
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_801.i
@@ -0,0 +1,18 @@
+int a ;
+
+/*@
+  requires a == 1;
+  ensures a == 1;
+*/
+void LoopCurrent()
+{
+  /*@
+    loop assigns s,a;
+    loop invariant A: \at(a, LoopCurrent)== 1;
+    loop variant 10-s;
+  */
+  for(int s = 0; s< 10; s++)
+    {
+      a = 2;
+    }
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..23bbba6733ff9920e819f21fcd5effcb81cd8422
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_801.res.oracle
@@ -0,0 +1,39 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_801.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function LoopCurrent
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_801.i, line 5) in 'LoopCurrent':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'A' (file tests/wp_bts/issue_801.i, line 11):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'A' (file tests/wp_bts/issue_801.i, line 11):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_801.i, line 10):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file tests/wp_bts/issue_801.i, line 14):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file tests/wp_bts/issue_801.i, line 14):
+Assume { Type: is_sint32(s). (* Then *) Have: s <= 9. }
+Prove: s <= 10.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/c45214be00ee9772cbc817e818d45cff.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/c45214be00ee9772cbc817e818d45cff.json
new file mode 100644
index 0000000000000000000000000000000000000000..08344e3edd6d2e8d0a5f96f5c2bc3ff3b1abf4c0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.0.session/cache/c45214be00ee9772cbc817e818d45cff.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0078,
+  "steps": 8 }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5da74e2177681040534ed999560a6b27cafa5773
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_801.res.oracle
@@ -0,0 +1,19 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_801.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_LoopCurrent_ensures : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_invariant_A_preserved : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_invariant_A_established : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_assigns : Valid
+[wp] [Qed] Goal typed_LoopCurrent_loop_variant_decrease : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_LoopCurrent_loop_variant_positive : Valid
+[wp] Proved goals:    6 / 6
+  Qed:               5 
+  Alt-Ergo 2.0.0:    1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  LoopCurrent               5        1        6       100%
+------------------------------------------------------------