diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
index 3e0d3075cbff6ee167291580f18d5b1bd7d0c17b..b9f3d2dba058dd1563df40fac03437a37c36cf28 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_508.res.oracle
@@ -17,8 +17,11 @@ Assume {
   (* Goal *)
   When: !invalid(Malloc_0, shiftfield_F1_size(shift_S1(a, x)), 1).
   (* Pre-condition *)
-  Have: (0 <= d) /\ (d <= 16) /\ valid_rw(Malloc_0, tbl_0, 35) /\
-      valid_rw(Malloc_0, shift_S1(a, 0), 34).
+  Have: valid_rw(Malloc_0, tbl_0, 35).
+  (* Pre-condition *)
+  Have: valid_rw(Malloc_0, shift_S1(a, 0), 34).
+  (* Pre-condition *)
+  Have: (0 <= d) /\ (d <= 16).
 }
 Prove: (x <= d) /\ (d <= x).