diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ee6d749805a8fb90468fd8eb263e8b22a4cc6ca5..110ef26efaed4f63b55589df6495d57071948a0d 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1162,7 +1162,7 @@ struct
| (caller_d, rel), Some (callee_d,_ ) ->
let rel caller callee = match rel with
| None ->
- p_and (p_leq e_zero callee) (p_lt callee caller)
+ p_and (p_leq e_zero caller) (p_lt callee caller)
| Some rel ->
(L.in_frame call_f (L.call_pred call_e))
rel [] [caller ; callee]
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
index 61a3435b5bbc033d1871b398ddf626f180645976..65805aa212de29ff538de8e68b6cd7ea4bc82640 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/clusters.res.oracle
@@ -122,7 +122,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 12
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
index d20b06232776956bd66553f5a393316e9f2574d6..84ff1f41b857153c800622b41c6622c7af1a46e0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
@@ -24,7 +24,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 17
Assume { Type: is_uint32(n). (* Else *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -52,7 +52,7 @@ Prove: 0 < n.
Goal Recursion variant:
Call Effect at line 40
Assume { Type: is_sint32(n). (* Else *) Have: n != 0. }
-Prove: 0 < n.
+Prove: 0 <= n.
------------------------------------------------------------
------------------------------------------------------------
@@ -120,7 +120,7 @@ Prove: P_Rel(n, n).
Goal Recursion variant:
Call Effect at line 55
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -130,14 +130,14 @@ Prove: to_uint32(n - 1) < n.
Goal Recursion variant (1/2):
Call Effect at line 59
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 60
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
@@ -157,7 +157,7 @@ Prove: false.
Goal Recursion variant (2/2):
Call Effect at line 72
Assume { Type: is_uint32(n). (* Then *) Have: 31 <= n. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -179,7 +179,7 @@ Prove: to_uint32(n - 1) <= 10.
Goal Recursion variant:
Call Effect at line 86
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -200,14 +200,14 @@ Prove: true.
Goal Recursion variant (1/2):
Call Effect at line 91
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 92
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
index acfb72158d91d27f3953083bfe93b24b4d9e0178..f45e5a772fee6d25d380583944f4b4417991a2f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
@@ -24,7 +24,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 17
Assume { Type: is_uint32(n). (* Else *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -51,14 +51,7 @@ Prove: 0 < n.
Goal Recursion variant:
Call Effect at line 40
-Assume {
- Type: is_sint32(n).
- (* Goal *)
- When: 0 <= n.
- (* Else *)
- Have: n != 0.
-}
-Prove: 0 < n.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -132,7 +125,7 @@ Prove: P_Rel(n, n).
Goal Recursion variant:
Call Effect at line 55
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -142,14 +135,14 @@ Prove: to_uint32(n - 1) < n.
Goal Recursion variant (1/2):
Call Effect at line 59
Assume { Type: is_uint32(x). (* Then *) Have: x != 0. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
Goal Recursion variant (2/2):
Call Effect at line 60
Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
------------------------------------------------------------
@@ -169,7 +162,7 @@ Prove: false.
Goal Recursion variant (2/2):
Call Effect at line 72
Assume { Type: is_uint32(n). (* Then *) Have: 31 <= n. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -191,7 +184,7 @@ Prove: to_uint32(n - 1) <= 10.
Goal Recursion variant:
Call Effect at line 86
Assume { Type: is_uint32(n). (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
@@ -218,7 +211,7 @@ Assume {
(* Then *)
Have: x != 0.
}
-Prove: to_uint32(x - 1) < x.
+Prove: (0 <= x) /\ (to_uint32(x - 1) < x).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index d8eeb1c7538d13ae49466588dcd4070e164b29ba..484dd6e31ec2b96eeb5bc83bfc02f60bb486c818 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -77,7 +77,7 @@ Prove: true.
Goal Recursion variant:
Call Effect at line 80
Assume { Type: is_uint32(n). (* Goal *) When: P_Q. (* Then *) Have: n != 0. }
-Prove: to_uint32(n - 1) < n.
+Prove: (0 <= n) /\ (to_uint32(n - 1) < n).
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
index 541e824ca018457efbf91c512ea2ac7bd2794e1f..f18fe8e1bdfe5c40aead8f912bb2e0cfdcc05743 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
@@ -20,7 +20,7 @@
[wp] [Alt-Ergo] Goal typed_fails_facto_gen_variant : Unsuccess
[wp] [Qed] Goal typed_fact_i_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_fact_i_terminates_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_fact_i_variant : Valid
+[wp] [Qed] Goal typed_fact_i_variant : Valid
[wp] [Qed] Goal typed_fails_fact_i_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_i_terminates_part2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_fails_fact_i_variant : Unsuccess
@@ -41,15 +41,15 @@
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
[wp] [Qed] Goal typed_se_variant : Valid
[wp] Proved goals: 19 / 27
- Qed: 8
- Alt-Ergo: 11 (unsuccess: 8)
+ Qed: 9
+ Alt-Ergo: 10 (unsuccess: 8)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
fact 1 1 2 100%
fails_fact - - 1 0.0%
facto_gen - 1 1 100%
fails_facto_gen - - 1 0.0%
- fact_i 1 2 3 100%
+ fact_i 2 1 3 100%
fails_fact_i 1 - 3 33.3%
m2 - 2 2 100%
m1 - 1 1 100%