[wp] naming pre-conditions

src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle

@@ -17,7 +17,11 @@ Assume {
       IsArray_sint32(Array_sint32(a, 10, Mint_0)) /\ is_sint32(x) /\
       IsArray_sint32(Array_sint32(a, 10, m)).
   (* Pre-condition *)
-  Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
+  Have: (0 <= i) /\ (i <= 9).
+  (* Pre-condition *)
+  Have: (0 <= j) /\ (j <= 9).
+  (* Pre-condition *)
+  Have: (0 <= k) /\ (k <= 9).
 }
 Prove: P_p_pointer(m, Mint_0, shift_sint32(a, 0), i, j).
 
@@ -35,7 +39,11 @@ Assume {
   Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\ IsArray_sint32(m) /\
       is_sint32(x) /\ IsArray_sint32(m_1).
   (* Pre-condition *)
-  Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
+  Have: (0 <= i) /\ (i <= 9).
+  (* Pre-condition *)
+  Have: (0 <= j) /\ (j <= 9).
+  (* Pre-condition *)
+  Have: (0 <= k) /\ (k <= 9).
 }
 Prove: P_p_arrays(m, i, m_1, j).
 
@@ -53,7 +61,11 @@ Assume {
       IsArray_sint32(Array_sint32(a, 10, Mint_0)) /\ is_sint32(x) /\
       IsArray_sint32(m).
   (* Pre-condition *)
-  Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
+  Have: (0 <= i) /\ (i <= 9).
+  (* Pre-condition *)
+  Have: (0 <= j) /\ (j <= 9).
+  (* Pre-condition *)
+  Have: (0 <= k) /\ (k <= 9).
 }
 Prove: P_p_dummy(m, j, k).