diff --git a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
index 1a343c630528b7e9168bb0126b3d7d389f3a8413..66a855de8d71d8783906372f8332d77884997523 100644
--- a/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/sharing.res.oracle
@@ -85,9 +85,12 @@ Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 9).
   (* Pre-condition *)
-  Have: (0 <= x) /\ (x <= 9) /\ valid_rw(Malloc_0, a, 10) /\
-      (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
-       (0 <= Mint_0[shift_sint32(t, i_1)])))).
+  Have: valid_rw(Malloc_0, a, 10).
+  (* Pre-condition *)
+  Have: (0 <= x) /\ (x <= 9).
+  (* Pre-condition *)
+  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) ->
+      (0 <= Mint_0[shift_sint32(t, i_1)]))).
 }
 Prove: 0 <= m_3[shift_sint32(t, 4) <- m_3[a_1]][shift_sint32(t, i)].