diff --git a/src/plugins/wp/tests/wp_bts/issue_453.i b/src/plugins/wp/tests/wp_bts/issue_453.i
deleted file mode 100644
index af0f2ff6923102bb739f9a1e4dea959577172ac0..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/issue_453.i
+++ /dev/null
@@ -1,35 +0,0 @@
-typedef unsigned T;
-T incr_value;
-
-//@ axiomatic A { predicate Incr(T x, T r) = r == x + incr_value; }
-
-/*@ assigns \nothing;
- @ ensures Incr(x, \result);
- @ */
-T incr(T x);
-
-// Was KO before the fix of #453
-void f1(T i) {
- /*@ loop assigns i;
- @*/
- while (i<10) {
- /*@ assigns i ;
- ensures Sincr: Incr(\old(i), i);
- */
- i = incr(i);
- }
-}
-
-// Was OK before the fix of #453
-void f2(T i) {
- /*@ loop assigns i;
- @*/
- while (i<10) {
- //@ ghost A: ;
- /*@ assigns i ;
- ensures Sincr: Incr(\old(i), i);
- */
- i = incr(i);
- //@ ghost B: ;
- }
-}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
deleted file mode 100644
index 9c1dde973cc4e3eb98f278b9b5e659b8b357387b..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle
+++ /dev/null
@@ -1,46 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function f1
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_bts/issue_453.i, line 13):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f1 with behavior default_for_stmt_7
-------------------------------------------------------------
-
-Goal Post-condition 'Sincr' at call 'incr' (file tests/wp_bts/issue_453.i, line 19):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/issue_453.i, line 16) at call 'incr' (file tests/wp_bts/issue_453.i, line 19):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f2
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_bts/issue_453.i, line 25):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function f2 with behavior default_for_stmt_17
-------------------------------------------------------------
-
-Goal Post-condition 'Sincr' at call 'incr' (file tests/wp_bts/issue_453.i, line 32):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/issue_453.i, line 29) at call 'incr' (file tests/wp_bts/issue_453.i, line 32):
-Prove: true.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
deleted file mode 100644
index c4d33cc9b69a9af5442f34759db1c02b3fd3aa32..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 6 goals scheduled
-[wp] [Qed] Goal typed_f1_loop_assigns : Valid
-[wp] [Qed] Goal typed_f1_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f1_assigns : Valid
-[wp] [Qed] Goal typed_f2_loop_assigns : Valid
-[wp] [Qed] Goal typed_f2_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f2_assigns : Valid
-[wp] Proved goals: 6 / 6
- Qed: 6
-------------------------------------------------------------
- Functions WP Alt-Ergo Total Success
- f1 3 - 3 100%
- f2 3 - 3 100%
-------------------------------------------------------------