diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
index c377eb93bf7fa1a03983b67f6950c86b1e851748..641adaa819218411aaf86ba480296ea0fa940ee2 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
@@ -67,12 +67,12 @@ Goal Post-condition for 'X' (file tests/wp/wp_behavior.i, line 28) in 'behaviors
 Assume {
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'Y' *)
-  Have: (P_CY -> P_RY).
-  (* Pre-condition for 'X' *)
-  Have: P_RX.
   (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
+  (* Pre-condition for 'Y' *)
+  Have: (P_CY -> P_RY).
   (* Assertion *)
   Have: P_Q.
 }
@@ -91,12 +91,12 @@ Assume {
   When: !invalid(Malloc_0, px_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'Y' *)
-  Have: (P_CY -> P_RY).
-  (* Pre-condition for 'X' *)
-  Have: P_RX.
   (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
+  (* Pre-condition for 'Y' *)
+  Have: (P_CY -> P_RY).
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -116,12 +116,12 @@ Assume {
   When: !invalid(Malloc_0, py_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'Y' *)
-  Have: (P_CY -> P_RY).
-  (* Pre-condition for 'X' *)
-  Have: P_RX.
   (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
+  (* Pre-condition for 'Y' *)
+  Have: (P_CY -> P_RY).
   (* Assertion *)
   Have: P_Q.
 }
@@ -136,12 +136,12 @@ Goal Post-condition for 'Y' (file tests/wp/wp_behavior.i, line 33) in 'behaviors
 Assume {
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'X' *)
-  Have: (P_CX -> P_RX).
-  (* Pre-condition for 'Y' *)
-  Have: P_RY.
   (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
+  (* Pre-condition for 'X' *)
+  Have: (P_CX -> P_RX).
   (* Assertion *)
   Have: P_Q.
 }
@@ -160,12 +160,12 @@ Assume {
   When: !invalid(Malloc_0, px_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'X' *)
-  Have: (P_CX -> P_RX).
-  (* Pre-condition for 'Y' *)
-  Have: P_RY.
   (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
+  (* Pre-condition for 'X' *)
+  Have: (P_CX -> P_RX).
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -185,12 +185,12 @@ Assume {
   When: !invalid(Malloc_0, py_0, 1).
   (* Pre-condition *)
   Have: P_R.
-  (* Pre-condition for 'X' *)
-  Have: (P_CX -> P_RX).
-  (* Pre-condition for 'Y' *)
-  Have: P_RY.
   (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
+  (* Pre-condition for 'X' *)
+  Have: (P_CX -> P_RX).
   (* Assertion *)
   Have: P_Q.
 }
@@ -321,9 +321,9 @@ Assume {
   (* Pre-condition for 'X' *)
   Have: P_CX.
   (* Pre-condition for 'X' *)
-  Have: P_RX1.
-  (* Pre-condition for 'X' *)
   Have: P_RX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX1.
 }
 Prove: q = p.
 
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
index 8d98a45587a8418840253e104b34f8591534e2d9..96a885bba3278990a3effd16f15de58b00016115 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
@@ -38,9 +38,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'X' *)
-  Have: P_RX.
-  (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
   (* Assertion *)
   Have: P_Q.
 }
@@ -60,9 +60,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'X' *)
-  Have: P_RX.
-  (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -83,9 +83,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'X' *)
-  Have: P_RX.
-  (* Pre-condition for 'X' *)
   Have: P_CX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX.
   (* Assertion *)
   Have: P_Q.
 }
@@ -101,9 +101,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'Y' *)
-  Have: P_RY.
-  (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
   (* Assertion *)
   Have: P_Q.
 }
@@ -123,9 +123,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'Y' *)
-  Have: P_RY.
-  (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
   (* Assertion *)
   Have: P_Q.
   (* Then *)
@@ -146,9 +146,9 @@ Assume {
   (* Pre-condition *)
   Have: P_R.
   (* Pre-condition for 'Y' *)
-  Have: P_RY.
-  (* Pre-condition for 'Y' *)
   Have: P_CY.
+  (* Pre-condition for 'Y' *)
+  Have: P_RY.
   (* Assertion *)
   Have: P_Q.
 }
@@ -279,9 +279,9 @@ Assume {
   (* Pre-condition for 'X' *)
   Have: P_CX.
   (* Pre-condition for 'X' *)
-  Have: P_RX1.
-  (* Pre-condition for 'X' *)
   Have: P_RX.
+  (* Pre-condition for 'X' *)
+  Have: P_RX1.
 }
 Prove: q = p.