diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
index dc175209d045c22bc6a1b1c9f0f2ee40e2e6eb14..049b05cc6d22c139a68c10308a6cdd3a9eedbd1a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
@@ -204,7 +204,7 @@ Assume {
Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
(* Exit Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((j < i_1) \/ (i_1 < 0)) -> (t4_0[i_1] = t4_1[i_1])))).
+ (((i_1 < 0) \/ (j < i_1)) -> (t4_0[i_1] = t4_1[i_1])))).
}
Prove: i <= 0.
@@ -220,7 +220,7 @@ Assume {
Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
(* Call Effects *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((j < i_1) \/ (i_1 < 0)) -> (t4_0[i_1] = t4_1[i_1])))).
+ (((i_1 < 0) \/ (j < i_1)) -> (t4_0[i_1] = t4_1[i_1])))).
}
Prove: i <= 0.
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index fe5efd3387bb1d178ffa29453a8fe165d26d5a61..7c9323b15bddef6ceb6e7b72f5ff93cde586989a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -367,13 +367,15 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -421,8 +423,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -456,8 +458,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -1049,13 +1051,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -1088,13 +1092,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -1136,13 +1142,15 @@ Assume {
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -1175,8 +1183,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (0 <= i_1) /\ (j <= i_1) /\ (i_2 <= 9) /\ (i_1 <= 19).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (0 <= i_1) /\ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------
@@ -1194,8 +1202,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
@@ -1642,8 +1650,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (j <= i_1) /\ (i_2 <= 9).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index 39da789135d1e735b9b24c80aba49e542bfea76b..b48ff1d096a88cc4556844017f3f3338bfe90005 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -367,13 +367,15 @@ Assume {
(havoc(Mint_undef_0, Mint_1, shift_sint32(a_1, 0), 20)
[shift_sint32(a_1, i_3)] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -421,8 +423,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -456,8 +458,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
Have: forall a : addr.
@@ -1049,13 +1051,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -1088,13 +1092,15 @@ Assume {
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (t2_2[i][i_3] = v))).
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -1136,13 +1142,15 @@ Assume {
(* Then *)
Have: j <= 19.
}
-Prove: (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) -> false))))) \/
- (forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
- ((i_3 <= 19) ->
- (exists i_6,i_5 : Z. (i_6 <= i_4) /\ (i_5 <= i_3) /\ (0 <= i_6) /\
- (i_4 <= i_6) /\ (0 <= i_5) /\ (i_3 <= i_5) /\ (i_6 <= 9) /\
- (i_5 <= 19))))))).
+Prove: (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) -> false)))))))) \/
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (forall i_4 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_3 <= 9) ->
+ ((i_4 <= 19) ->
+ (exists i_6,i_5 : Z. (i_6 <= i_3) /\ (i_5 <= i_4) /\ (0 <= i_6) /\
+ (i_3 <= i_6) /\ (0 <= i_5) /\ (i_4 <= i_5) /\ (i_6 <= 9) /\
+ (i_5 <= 19)))))))))).
------------------------------------------------------------
@@ -1175,8 +1183,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (0 <= i_1) /\ (j <= i_1) /\ (i_2 <= 9) /\ (i_1 <= 19).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (0 <= i_1) /\ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9) /\ (i_1 <= 19).
------------------------------------------------------------
@@ -1194,8 +1202,8 @@ Assume {
Have: i_2 <= 9.
Have: i_3 <= 19.
Have: 0 <= i.
- Have: 0 <= i_1.
Have: i <= 9.
+ Have: 0 <= i_1.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone_i' *)
Have: forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
@@ -1642,8 +1650,8 @@ Assume {
(* Invariant 'Range_j' *)
Have: j <= 20.
}
-Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (i_1 <= j) /\ (0 <= i_2) /\
- (i <= i_2) /\ (j <= i_1) /\ (i_2 <= 9).
+Prove: exists i_2,i_1 : Z. (i_2 <= i) /\ (0 <= i_2) /\ (i <= i_2) /\
+ (j <= i_1) /\ (i_1 <= j) /\ (i_2 <= 9).
------------------------------------------------------------