diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
index 4f4bf9be94af2fb141cb61287434873e95579349..8ee9e5fdf9b33fe732705bb05a771463647de355 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
@@ -18,14 +18,7 @@ Prove: true.
 
 Goal Instance of 'Pre-condition 'qed_ok,Rf' in 'f'' in 'double_call' at initialization of 'x2' (file wp_call_pre.c, line 26)
 :
-Assume {
-  Type: is_sint32(f) /\ is_sint32(x).
-  (* Pre-condition 'Rd' *)
-  Have: 0 <= x.
-  (* Call 'f' *)
-  Have: 0 < f.
-}
-Prove: (-1) <= x.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
index 15d814ca6a84a699d2d2f8b7bafb37f6fb82eefd..63c5f1576f9bcce5d71cad71eb0588f4a083bb04 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
@@ -13,13 +13,6 @@ Prove: true.
 
 Goal Instance of 'Pre-condition 'qed_ok,Rf' in 'f'' in 'double_call' at initialization of 'x2' (file wp_call_pre.c, line 26)
 :
-Assume {
-  Type: is_sint32(f) /\ is_sint32(x).
-  (* Pre-condition 'Rd' *)
-  Have: 0 <= x.
-  (* Call 'f' *)
-  Have: 0 < f.
-}
-Prove: (-1) <= x.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
index 9e0b53a7ea00e802ab646ce680706f403492eed3..745239a656b1bd3f1050de4cf623cbcce886bdba 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
@@ -158,13 +158,11 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Assertion 'qed_ok,A1' (file arith.i, line 16):
-Assume { Type: is_uint8(i). }
-Prove: 0 <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Assertion 'qed_ok,A2' (file arith.i, line 17):
-Assume { Type: is_uint8(i). (* Assertion 'qed_ok,A1' *) Have: 0 <= i. }
-Prove: i <= 255.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
index b8e9db163f8c7c8827d8cfad9f00adbc62f6f73f..aaf2d71df37874351849fd00cad82103468c01c0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
@@ -35,23 +35,7 @@ Prove: Mint_0[shift_sint32(b, i)] = v[i].
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file assigns_path.i, line 16):
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: region(b.base) <= 0.
-  (* Pre-condition *)
-  Have: n <= 3.
-  (* Invariant *)
-  Have: 0 <= n.
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (Mint_0[shift_sint32(b, i_1)] = v[i_1]))).
-  (* Then *)
-  Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
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 f06695c9f125f82f6b716b56813b8ea9009772d6..cb23d6906cfdf29fa29540c3642099871abb7a03 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
@@ -89,22 +89,7 @@ Prove: true.
 
 Goal Instance of 'Pre-condition (file assigns_range.i, line 23) in 'assigns_t4_sup_bound'' in 'call_assigns_all' at call 'assigns_t4_sup_bound' (file assigns_range.i, line 40)
 :
-Assume {
-  Type: is_sint32(i) /\ is_sint32(j).
-  (* Heap *)
-  Type: IsArray_sint32(t2_0) /\ IsArray_sint32(t3_0).
-  (* Pre-condition *)
-  Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
-  (* Call 'assigns_t1_an_element' *)
-  Have: i <= 19.
-  (* Call Effects *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
-      (((i_1 < i) \/ (j < i_1)) -> (t2_1[i_1] = t2_0[i_1])))).
-  (* Call Effects *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
-      (((i_1 < i) \/ (20 <= i_1)) -> (t3_1[i_1] = t3_0[i_1])))).
-}
-Prove: 0 <= j.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -237,11 +222,6 @@ Prove: i <= 0.
 
 Goal Instance of 'Pre-condition (file assigns_range.i, line 23) in 'assigns_t4_sup_bound'' in 'call_assigns_t4' at call 'assigns_t4_sup_bound' (file assigns_range.i, line 65)
 :
-Assume {
-  Type: is_sint32(i) /\ is_sint32(j).
-  (* Pre-condition *)
-  Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
-}
-Prove: 0 <= j.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 4c3b2575f9e95220d9b3b656cd14fa11ed3ed423..18d052e09ff36536fde976446a86f6b3e701e2bb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -90,102 +90,7 @@ Prove: (a_16 = (1 + x[i])) /\ (a_17 = (1 + a_16)) /\ (a_18 = (1 + a_17)) /\
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file chunk_typing.i, line 31):
-Let a = shift_uint64(u64_0, i).
-Let a_1 = shift_sint64(i64_0, i).
-Let a_2 = shift_uint32(u32_0, i).
-Let a_3 = shift_sint32(i32_0, i).
-Let a_4 = shift_uint16(u16_0, i).
-Let a_5 = shift_sint16(i16_0, i).
-Let a_6 = shift_uint8(u8_0, i).
-Let a_7 = shift_sint8(i8_0, i).
-Let a_8 = shift_uint64(u64_0, 0).
-Let a_9 = havoc(Mint_undef_5, Mint_5, a_8, 10).
-Let a_10 = shift_sint64(i64_0, 0).
-Let a_11 = havoc(Mint_undef_2, Mint_2, a_10, 10).
-Let a_12 = shift_uint32(u32_0, 0).
-Let a_13 = havoc(Mint_undef_4, Mint_4, a_12, 10).
-Let a_14 = shift_sint32(i32_0, 0).
-Let a_15 = havoc(Mint_undef_1, Mint_1, a_14, 10).
-Let a_16 = shift_uint16(u16_0, 0).
-Let a_17 = havoc(Mint_undef_3, Mint_3, a_16, 10).
-Let a_18 = shift_sint16(i16_0, 0).
-Let a_19 = havoc(Mint_undef_0, Mint_0, a_18, 10).
-Let a_20 = shift_uint8(u8_0, 0).
-Let a_21 = havoc(Mint_undef_6, Mint_6, a_20, 10).
-Let a_22 = shift_sint8(i8_0, 0).
-Let a_23 = havoc(Mchar_undef_0, Mchar_0, a_22, 10).
-Assume {
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
-      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
-      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
-      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
-      is_sint32(1 + i) /\ is_sint16_chunk(a_19) /\ is_sint32_chunk(a_15) /\
-      is_sint64_chunk(a_11) /\ is_sint8_chunk(a_23) /\
-      is_uint16_chunk(a_17) /\ is_uint32_chunk(a_13) /\
-      is_uint64_chunk(a_9) /\ is_uint8_chunk(a_21) /\
-      is_sint16_chunk(a_19[a_5 <- 3]) /\ is_sint32_chunk(a_15[a_3 <- 5]) /\
-      is_sint64_chunk(a_11[a_1 <- 7]) /\ is_sint8_chunk(a_23[a_7 <- 1]) /\
-      is_uint16_chunk(a_17[a_4 <- 4]) /\ is_uint32_chunk(a_13[a_2 <- 6]) /\
-      is_uint64_chunk(a_9[a <- 8]) /\ is_uint8_chunk(a_21[a_6 <- 2]).
-  (* Heap *)
-  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
-      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
-      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
-      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
-      linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: valid_rw(Malloc_0, a_18, 10) /\ valid_rw(Malloc_0, a_14, 10) /\
-      valid_rw(Malloc_0, a_10, 10) /\ valid_rw(Malloc_0, a_22, 10) /\
-      valid_rw(Malloc_0, a_16, 10) /\ valid_rw(Malloc_0, a_12, 10) /\
-      valid_rw(Malloc_0, a_8, 10) /\ valid_rw(Malloc_0, a_20, 10).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_23[shift_sint8(i8_0, i_1)] = 1))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_21[shift_uint8(u8_0, i_1)] = 2))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_19[shift_sint16(i16_0, i_1)] = 3))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_17[shift_uint16(u16_0, i_1)] = 4))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_15[shift_sint32(i32_0, i_1)] = 5))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_13[shift_uint32(u32_0, i_1)] = 6))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_11[shift_sint64(i64_0, i_1)] = 7))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_9[shift_uint64(u64_0, i_1)] = 8))).
-  (* Then *)
-  Have: i <= 9.
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_7, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_6, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_5, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_4, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_3, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_2, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_1, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a, 1).
-  (* Assertion 'rte,signed_overflow' *)
-  Have: i <= 2147483646.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -1846,100 +1751,7 @@ Prove: valid_rw(Malloc_0, shift_uint64(u64_0, i), 1).
 ------------------------------------------------------------
 
 Goal Assertion 'rte,signed_overflow' (file chunk_typing.i, line 44):
-Let a = shift_uint64(u64_0, i).
-Let a_1 = shift_sint64(i64_0, i).
-Let a_2 = shift_uint32(u32_0, i).
-Let a_3 = shift_sint32(i32_0, i).
-Let a_4 = shift_uint16(u16_0, i).
-Let a_5 = shift_sint16(i16_0, i).
-Let a_6 = shift_uint8(u8_0, i).
-Let a_7 = shift_sint8(i8_0, i).
-Let a_8 = shift_uint64(u64_0, 0).
-Let a_9 = havoc(Mint_undef_5, Mint_5, a_8, 10).
-Let a_10 = shift_sint64(i64_0, 0).
-Let a_11 = havoc(Mint_undef_2, Mint_2, a_10, 10).
-Let a_12 = shift_uint32(u32_0, 0).
-Let a_13 = havoc(Mint_undef_4, Mint_4, a_12, 10).
-Let a_14 = shift_sint32(i32_0, 0).
-Let a_15 = havoc(Mint_undef_1, Mint_1, a_14, 10).
-Let a_16 = shift_uint16(u16_0, 0).
-Let a_17 = havoc(Mint_undef_3, Mint_3, a_16, 10).
-Let a_18 = shift_sint16(i16_0, 0).
-Let a_19 = havoc(Mint_undef_0, Mint_0, a_18, 10).
-Let a_20 = shift_uint8(u8_0, 0).
-Let a_21 = havoc(Mint_undef_6, Mint_6, a_20, 10).
-Let a_22 = shift_sint8(i8_0, 0).
-Let a_23 = havoc(Mchar_undef_0, Mchar_0, a_22, 10).
-Assume {
-  Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
-      is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
-      is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
-      is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
-      is_sint16_chunk(a_19) /\ is_sint32_chunk(a_15) /\
-      is_sint64_chunk(a_11) /\ is_sint8_chunk(a_23) /\
-      is_uint16_chunk(a_17) /\ is_uint32_chunk(a_13) /\
-      is_uint64_chunk(a_9) /\ is_uint8_chunk(a_21) /\
-      is_sint16_chunk(a_19[a_5 <- 3]) /\ is_sint32_chunk(a_15[a_3 <- 5]) /\
-      is_sint64_chunk(a_11[a_1 <- 7]) /\ is_sint8_chunk(a_23[a_7 <- 1]) /\
-      is_uint16_chunk(a_17[a_4 <- 4]) /\ is_uint32_chunk(a_13[a_2 <- 6]) /\
-      is_uint64_chunk(a_9[a <- 8]) /\ is_uint8_chunk(a_21[a_6 <- 2]).
-  (* Heap *)
-  Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
-      (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
-      (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
-      (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
-      linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: valid_rw(Malloc_0, a_18, 10) /\ valid_rw(Malloc_0, a_14, 10) /\
-      valid_rw(Malloc_0, a_10, 10) /\ valid_rw(Malloc_0, a_22, 10) /\
-      valid_rw(Malloc_0, a_16, 10) /\ valid_rw(Malloc_0, a_12, 10) /\
-      valid_rw(Malloc_0, a_8, 10) /\ valid_rw(Malloc_0, a_20, 10).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_23[shift_sint8(i8_0, i_1)] = 1))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_21[shift_uint8(u8_0, i_1)] = 2))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_19[shift_sint16(i16_0, i_1)] = 3))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_17[shift_uint16(u16_0, i_1)] = 4))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_15[shift_sint32(i32_0, i_1)] = 5))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_13[shift_uint32(u32_0, i_1)] = 6))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_11[shift_sint64(i64_0, i_1)] = 7))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_9[shift_uint64(u64_0, i_1)] = 8))).
-  (* Then *)
-  Have: i <= 9.
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_7, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_6, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_5, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_4, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_3, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_2, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a_1, 1).
-  (* Assertion 'rte,mem_access' *)
-  Have: valid_rw(Malloc_0, a, 1).
-}
-Prove: i <= 2147483646.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
index b97ad87904779045a6204e8e3bef96608684a346..bb59f39de147587a3ece2827d5e3c67c29a50f10 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
@@ -35,30 +35,7 @@ Prove: P_IsEqual(havoc(Mint_undef_0, Mint_0, a_1, i), a, b, i).
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file looplabels.i, line 18):
-Let a_1 = shift_sint32(b, 0).
-Let a_2 = shift_sint32(a, 0).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: (region(a.base) <= 0) /\ (region(b.base) <= 0) /\ linked(Malloc_0).
-  (* Pre-condition *)
-  Have: 0 < n.
-  (* Pre-condition *)
-  Have: valid_rw(Malloc_0, a_2, n).
-  (* Pre-condition *)
-  Have: valid_rw(Malloc_0, a_1, n).
-  (* Pre-condition *)
-  Have: separated(a_2, n, a_1, n).
-  (* Invariant *)
-  Have: P_IsEqual(Mint_0, a, b, 0).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant *)
-  Have: P_IsEqual(havoc(Mint_undef_0, Mint_0, a_1, n), a, b, i).
-  (* Then *)
-  Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
index 45bac9e9756deeb47911d7acc0a215292a3d51fe..68a4d2e6a12bc598dda6c510b4900c096951b82a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
@@ -145,16 +145,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file postassigns.c, line 38):
-Assume {
-  Type: is_sint32(N) /\ is_sint32(i) /\ is_sint32(1 + i).
-  (* Invariant *)
-  Have: 0 <= N.
-  (* Invariant *)
-  Have: (i <= N) /\ (0 <= i).
-  (* Then *)
-  Have: i < N.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
index e3393701a39b16a09cf88c4f8cccd6b4f1c74752..80262cbe5dcbc1b5163ee93464008fa7b0469d4d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
@@ -229,28 +229,7 @@ Prove: 0 < havoc(Mint_undef_0, Mint_0, a, i)[shift_sint32(t, i_1)].
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file simpl_is_type.i, line 22):
-Let a = havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), size_0).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(size_0) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: region(t.base) <= 0.
-  (* Pre-condition *)
-  Have: 0 < size_0.
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < size_0) ->
-      (Mint_0[shift_sint32(t, i_1)] < 0))).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= size_0).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (0 < a[shift_sint32(t, i_1)]))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((i <= i_1) -> ((i_1 < size_0) ->
-      (a[shift_sint32(t, i_1)] < 0))).
-  (* Then *)
-  Have: i < size_0.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -422,25 +401,7 @@ Prove: exists i_1 : Z. (Mint_0[shift_sint32(t, i_1)] = x) /\ (0 <= i_1) /\
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file simpl_is_type.i, line 44):
-Let x_1 = Mint_0[shift_sint32(t, i)].
-Assume {
-  Type: is_sint32(i) /\ is_sint32(size_0) /\ is_sint32(x) /\
-      is_sint32(1 + i) /\ is_sint32(x_1).
-  (* Heap *)
-  Type: region(t.base) <= 0.
-  (* Pre-condition *)
-  Have: 0 < size_0.
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= size_0).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (Mint_0[shift_sint32(t, i_1)] != x))).
-  (* Then *)
-  Have: i < size_0.
-  (* Else *)
-  Have: x_1 != x.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
index 37df7d0a04ad853ae4c9a561b3f801830be8eeca..dc049f029f87f114c2375d65c23ae0278d5343d1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
@@ -46,18 +46,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Positivity of Loop variant at loop (file terminates_variant_option.i, line 41):
-Assume {
-  Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
-  (* Goal *)
-  When: c1_0 != 0.
-  (* Invariant *)
-  Have: ((0 <= c1_0) -> ((cpt_0 <= c1_0) /\ (0 <= cpt_0))).
-  (* Else *)
-  Have: 2 <= cpt_0.
-  (* Invariant *)
-  Have: ((0 <= c1_0) -> (cpt_0 <= (1 + c1_0))).
-}
-Prove: 0 <= cpt_0.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
index 5683dde8aeb75d334dfbcca8ca1510e3ecf372c6..214d5ef2e3c295a8a5ccb2a74c65b79b5f10d88a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
@@ -7,8 +7,6 @@
 ------------------------------------------------------------
 
 Goal Assertion (file bts779.i, line 6):
-Let x = Mint_0[shift_uint8(t, 0)].
-Assume { Type: is_uint8(x). (* Heap *) Type: region(t.base) <= 0. }
-Prove: x <= 255.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
index 18231f2787cfacbce7f1fd426b27d0a7d6beaf6e..2e738afb004c169c4707afb644b505700e014741 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
@@ -7,18 +7,7 @@
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'RANGE' (file issue_751.i, line 7):
-Let x = land(3840, R).
-Let x_1 = x / 256.
-Assume {
-  Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j).
-  (* Pre-condition *)
-  Have: (0 < x) /\ (x <= 2303).
-  (* Invariant 'RANGE' *)
-  Have: (0 <= j) /\ (j <= x_1).
-  (* Then *)
-  Have: j < x_1.
-}
-Prove: (-1) <= j.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
index 977dad88e4b8bd65073c642151a2889636f5cdf4..ff49553d88311ef1563b0e947cde8ea45e6f6c20 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
@@ -13,24 +13,7 @@ Prove: (50 <= A) /\ (A <= 100).
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file combined.c, line 29):
-Assume {
-  Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(v) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: region(t.base) <= 0.
-  (* Assertion *)
-  Have: (50 <= A) /\ (A <= 100).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 50).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      P_P(havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), 50)
-            [shift_sint32(t, i_1)]))).
-  (* Then *)
-  Have: i <= 49.
-  (* Call 'f' *)
-  Have: P_P(v).
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
index 45e2914bd4368a4294ef5d1f7d79ced28026b58c..5e9cbd10437bd13908135ea1710ece6d0ef94af0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
@@ -72,32 +72,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'Range' (file copy.i, line 10):
-Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
-Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
-  (* Pre-condition *)
-  Have: separated(a_1, n, shift_sint32(b, 0), n).
-  (* Invariant 'Range' *)
-  Have: 0 <= n.
-  (* Invariant 'Range' *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant 'Copy' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
-  (* Then *)
-  Have: i < n.
-  (* Assertion 'A' *)
-  Have: forall i_1 : Z. let a_4 = shift_sint32(a, i_1) in ((0 <= i_1) ->
-      ((i_1 < i) -> (a_3[a_4] = a_2[a_4]))).
-  (* Assertion 'B' *)
-  Have: forall i_1 : Z. let a_4 = shift_sint32(b, i_1) in ((0 <= i_1) ->
-      ((i_1 < i) -> (a_3[a_4] = a_2[a_4]))).
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
index 2721d73c7500aabcf175de96f4a81508a0ad48ed..ed64f075c63c343af27c65f1a726533d26fc6e35 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
@@ -48,32 +48,7 @@ Prove: (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < n) ->
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'I' (file prenex.i, line 19):
-Assume {
-  Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(m) /\ is_sint32(n) /\
-      is_sint32(1 + i).
-  (* Heap *)
-  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
-  (* Invariant 'I' *)
-  Have: 0 <= n.
-  (* Invariant 'I' *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant 'PI' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 < m) ->
-      (Mint_0[shift_sint32(p, i_2)] < Mint_0[shift_sint32(q, i_1)]))))).
-  (* Then *)
-  Have: i < n.
-  (* Invariant 'J' *)
-  Have: 0 <= m.
-  (* Invariant 'J' *)
-  Have: (0 <= j) /\ (j <= m).
-  (* Invariant 'PJ' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) ->
-      (Mint_0[shift_sint32(p, i)] < Mint_0[shift_sint32(q, i_1)]))).
-  (* Else *)
-  Have: m <= j.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -122,36 +97,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'J' (file prenex.i, line 28):
-Let x = Mint_0[shift_sint32(p, i)].
-Let x_1 = Mint_0[shift_sint32(q, j)].
-Assume {
-  Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(m) /\ is_sint32(n) /\
-      is_sint32(1 + j) /\ is_sint32(x) /\ is_sint32(x_1).
-  (* Heap *)
-  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
-  (* Invariant 'I' *)
-  Have: 0 <= n.
-  (* Invariant 'I' *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant 'PI' *)
-  Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
-      ((i_1 < m) ->
-      (Mint_0[shift_sint32(p, i_2)] < Mint_0[shift_sint32(q, i_1)]))))).
-  (* Then *)
-  Have: i < n.
-  (* Invariant 'J' *)
-  Have: 0 <= m.
-  (* Invariant 'J' *)
-  Have: (0 <= j) /\ (j <= m).
-  (* Invariant 'PJ' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) ->
-      (x < Mint_0[shift_sint32(q, i_1)]))).
-  (* Then *)
-  Have: j < m.
-  (* Else *)
-  Have: x < x_1.
-}
-Prove: (-1) <= j.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
index 99192ce42a745e79c0ad5c0db4e0dc9abf038296..72cc29ecc9f80e0b3607e643e19a3db7d752e257 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
@@ -13,27 +13,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file repeat.c, line 61):
-Let a = L_sequence(calls_1).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: is_sint32(calls_0).
-  (* Pre-condition *)
-  Have: L_sequence(calls_0) = nil.
-  (* Invariant *)
-  Have: 0 <= n.
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant *)
-  Have: ([ 1, 2 ] *^ i) = a.
-  (* Then *)
-  Have: i < n.
-  (* Call 'f' *)
-  Have: L_sequence(calls_2) = a ^ [ 1 ].
-  (* Call 'g' *)
-  Have: L_sequence(calls_3) = a ^ [ 1, 2 ].
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -148,29 +128,7 @@ Prove: (a *^ 1 + i) = a_2.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file repeat.c, line 81):
-Let a = ([ 1, 2 ] *^ i).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: is_sint32(calls_0).
-  (* Pre-condition *)
-  Have: L_sequence(calls_0) = nil.
-  (* Call 'f' *)
-  Have: L_sequence(calls_1) = [ 1 ].
-  (* Invariant *)
-  Have: 0 <= n.
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant *)
-  Have: L_sequence(calls_2) = a ^ [ 1 ].
-  (* Then *)
-  Have: i < n.
-  (* Call 'g' *)
-  Have: L_sequence(calls_3) = a ^ [ 1, 2 ].
-  (* Call 'f' *)
-  Have: L_sequence(calls_4) = a ^ [ 1, 2, 1 ].
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
index fedcdb66fb660ab5c85989b6c35ce166281fa5ba..156a43c16d4f721dea573881f62418033adc87ea 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
@@ -39,30 +39,7 @@ Prove: nth(a_1, 1 + i) = z.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'ok,id_max' (file sequence.i, line 97):
-Let a = ([ y ] *^ i).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x) /\ is_sint32(y) /\
-      is_sint32(1 + i).
-  (* Heap *)
-  Type: is_sint32(call_seq_0).
-  (* Pre-condition *)
-  Have: L_call_obs(call_seq_0) = nil.
-  (* Call 'f' *)
-  Have: L_call_obs(call_seq_1) = [ x ].
-  (* Invariant 'ok,id_min' *)
-  Have: 0 <= i.
-  (* Invariant 'ok,id_max' *)
-  Have: if (0 <= n) then (i <= n) else (i <= 0).
-  (* Invariant 'ok,inv' *)
-  Have: L_call_obs(call_seq_2) = [ x ] ^ a.
-  (* Then *)
-  Have: i < n.
-  (* Call 'g' *)
-  Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ y ].
-  (* Invariant 'ok,id_min' *)
-  Have: (-1) <= i.
-}
-Prove: 0 <= n.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -72,28 +49,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'ok,id_min' (file sequence.i, line 96):
-Let a = ([ y ] *^ i).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x) /\ is_sint32(y) /\
-      is_sint32(1 + i).
-  (* Heap *)
-  Type: is_sint32(call_seq_0).
-  (* Pre-condition *)
-  Have: L_call_obs(call_seq_0) = nil.
-  (* Call 'f' *)
-  Have: L_call_obs(call_seq_1) = [ x ].
-  (* Invariant 'ok,id_min' *)
-  Have: 0 <= i.
-  (* Invariant 'ok,id_max' *)
-  Have: if (0 <= n) then (i <= n) else (i <= 0).
-  (* Invariant 'ok,inv' *)
-  Have: L_call_obs(call_seq_2) = [ x ] ^ a.
-  (* Then *)
-  Have: i < n.
-  (* Call 'g' *)
-  Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ y ].
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index c1383873535e632ba413a93d587aa48bb2c3a20d..faadd1df8084289a61a9d27e3c3bfd6d055fb10a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -66,19 +66,7 @@ Prove: to_uint64(1 + i) <= n.
 ------------------------------------------------------------
 
 Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
-Assume {
-  Type: is_uint64(n).
-  (* Heap *)
-  Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
-      linked(Malloc_0).
-  (* Pre-condition 'valid_dest' *)
-  Have: P_valid_or_empty(Malloc_0, dest_0, n).
-  (* Pre-condition 'valid_src' *)
-  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
-  (* Pre-condition 'separation' *)
-  Have: separated(shift_sint8(dest_0, 0), n, shift_sint8(src_0, 0), n).
-}
-Prove: 0 <= n.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -338,28 +326,7 @@ Prove: to_uint64(1 + i) <= n.
 ------------------------------------------------------------
 
 Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 95):
-Let a = shift_sint8(d, 0).
-Let a_1 = shift_sint8(s, 0).
-Assume {
-  Type: is_sint32(memoverlap_0) /\ is_uint64(n).
-  (* Heap *)
-  Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
-  (* Pre-condition 'valid_dest' *)
-  Have: P_valid_or_empty(Malloc_0, d, n).
-  (* Pre-condition 'valid_src' *)
-  Have: P_valid_read_or_empty(Malloc_0, s, n).
-  (* Else *)
-  Have: n != 0.
-  (* Call 'memoverlap' *)
-  Have: ((separated(a, n, a_1, n) -> (memoverlap_0 = 0))) /\
-      ((addr_le(d, s) -> (addr_lt(s, shift_sint8(d, n)) ->
-       ((!separated(a, n, a_1, n)) -> (memoverlap_0 = (-1)))))) /\
-      ((addr_lt(s, d) -> (addr_le(d, shift_sint8(s, n)) ->
-       ((!separated(a, n, a_1, n)) -> (memoverlap_0 = 1))))).
-  (* Then *)
-  Have: memoverlap_0 <= 0.
-}
-Prove: 0 <= n.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -850,48 +817,7 @@ Prove: true.
 
 Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 122) in 'memmove' (6/7):
 Effect at line 115
-Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
-Let x = to_uint64(n - 1).
-Let a_2 = shift_sint8(src_0, 0).
-Assume {
-  Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
-  (* Heap *)
-  Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
-      linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Goal *)
-  When: !invalid(Malloc_0, a, 1).
-  (* Pre-condition 'valid_dest' *)
-  Have: P_valid_or_empty(Malloc_0, d, n).
-  (* Pre-condition 'valid_src' *)
-  Have: P_valid_read_or_empty(Malloc_0, src_0, n).
-  (* Else *)
-  Have: n != 0.
-  (* Call 'memoverlap' *)
-  Have: ((separated(a, n, a_2, n) -> (memoverlap_0 = 0))) /\
-      ((addr_le(d, src_0) -> (addr_lt(src_0, shift_sint8(d, n)) ->
-       ((!separated(a, n, a_2, n)) -> (memoverlap_0 = (-1)))))) /\
-      ((addr_lt(src_0, d) -> (addr_le(d, shift_sint8(src_0, n)) ->
-       ((!separated(a, n, a_2, n)) -> (memoverlap_0 = 1))))).
-  (* Else *)
-  Have: 0 < memoverlap_0.
-  (* Invariant 'no_eva' *)
-  Have: x < n.
-  (* Invariant 'no_eva' *)
-  Have: forall i_1 : Z. ((i_1 < n) -> ((x < i_1) ->
-      (Mchar_0[shift_sint8(src_0, i_1)] = Mchar_0[shift_sint8(d, i_1)]))).
-  (* Invariant 'no_eva' *)
-  Have: (0 <= i) /\ (i < n).
-  (* Invariant 'no_eva' *)
-  Have: forall i_1 : Z. ((i < i_1) -> ((i_1 < n) ->
-      (a_1[shift_sint8(d, i_1)] = Mchar_0[shift_sint8(src_0, i_1)]))).
-  (* Invariant 'no_eva' *)
-  Have: forall i_1 : Z. let a_3 = shift_sint8(src_0, i_1) in ((i_1 <= i) ->
-      ((0 <= i_1) -> (a_1[a_3] = Mchar_0[a_3]))).
-  (* Else *)
-  Have: i <= 0.
-}
-Prove: 0 < n.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
index dd1cd3edf7d9ef503650337d4d5bca8a6a5e038f..b65abf98b7fcfae08fcaf1c97159d599c8c10f3e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -14,6 +14,7 @@
   Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
   
   ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
 [wp:script:allgoals] 
   typed_check_lemma_and_modulo_u subgoal:
   
@@ -30,30 +31,13 @@
   Prove: true.
   Prover Qed returns Valid
   
-  ------------------------------------------------------------
-[wp:script:allgoals] 
-  typed_check_lemma_and_modulo_us_255 subgoal:
-  
-  Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
-  Assume { Have: is_uint16(us_0). }
-  Prove: 0 <= us_0.
-  
-  ------------------------------------------------------------
-[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
-[wp:script:allgoals] 
-  typed_check_lemma_and_modulo_us_255 subgoal:
-  
-  Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
-  Prove: true.
-  Prover Qed returns Valid
-  
   ------------------------------------------------------------
 [wp:script:allgoals] 
   typed_check_lemma_and_modulo_u subgoal:
   
   Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
-  Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
-  Prove: 0 <= us_0.
+  Prove: true.
+  Prover Qed returns Valid
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
index e40e8863e3cf66cd9c1c3c6e4d1f0fa5d083d726..84b0af02539d9a89a4563ba38a73f7273b5d79b0 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
@@ -8,7 +8,9 @@
                                     "select": { "select": "clause-goal",
                                                 "target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n                         ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
                                                 "pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
-                                    "children": { "Goal 1/3": [ { "header": "Definition",
+                                    "children": { "Goal 1/3": [ { "prover": "qed",
+                                                                  "verdict": "valid" },
+                                                                { "header": "Definition",
                                                                   "tactic": "Wp.unfold",
                                                                   "params": {},
                                                                   "select": 
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
index 0232433c576b0cb20e7c6108b28bec094abaa799..67fe782ea8a713724aaa08a6bd0215e2afe57bbf 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
@@ -2,7 +2,8 @@
     "params": { "Wp.modmask.revert": false },
     "select": { "select": "inside-goal", "occur": 0,
                 "target": "us_0 mod 256", "pattern": "%$us256" },
-    "children": { "Mask Guard": [ { "header": "Definition",
+    "children": { "Mask Guard": [ { "prover": "qed", "verdict": "valid" },
+                                  { "header": "Definition",
                                     "tactic": "Wp.unfold", "params": {},
                                     "select": { "select": "clause-step",
                                                 "at": 0, "kind": "have",
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
index dd1cd3edf7d9ef503650337d4d5bca8a6a5e038f..b65abf98b7fcfae08fcaf1c97159d599c8c10f3e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -14,6 +14,7 @@
   Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
   
   ------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
 [wp:script:allgoals] 
   typed_check_lemma_and_modulo_u subgoal:
   
@@ -30,30 +31,13 @@
   Prove: true.
   Prover Qed returns Valid
   
-  ------------------------------------------------------------
-[wp:script:allgoals] 
-  typed_check_lemma_and_modulo_us_255 subgoal:
-  
-  Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
-  Assume { Have: is_uint16(us_0). }
-  Prove: 0 <= us_0.
-  
-  ------------------------------------------------------------
-[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
-[wp:script:allgoals] 
-  typed_check_lemma_and_modulo_us_255 subgoal:
-  
-  Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
-  Prove: true.
-  Prover Qed returns Valid
-  
   ------------------------------------------------------------
 [wp:script:allgoals] 
   typed_check_lemma_and_modulo_u subgoal:
   
   Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
-  Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
-  Prove: 0 <= us_0.
+  Prove: true.
+  Prover Qed returns Valid
   
   ------------------------------------------------------------
 [wp:script:allgoals] 
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
index 7d2e4b041e8f70d94528bc04cf06fc7d49bbbb6e..51fbe949924301501fb2a9aa26320303e520adaf 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
@@ -8,7 +8,9 @@
                                    "select": { "select": "clause-goal",
                                                "target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n                         ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
                                                "pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
-                                   "children": { "Goal 1/3": [ { "header": "Definition",
+                                   "children": { "Goal 1/3": [ { "prover": "qed",
+                                                                 "verdict": "valid" },
+                                                               { "header": "Definition",
                                                                  "tactic": "Wp.unfold",
                                                                  "params": {},
                                                                  "select": 
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
index a56490bac7af0b6011890ef00ef38f25fa4cd251..c16388ade5d0163bb875e3e7640aa57f4b96b603 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
@@ -2,7 +2,8 @@
     "params": { "Wp.modmask.revert": false },
     "select": { "select": "inside-goal", "occur": 0,
                 "target": "(land 255 us_0)", "pattern": "land255$us" },
-    "children": { "Mod Guard": [ { "header": "Definition",
+    "children": { "Mod Guard": [ { "prover": "qed", "verdict": "valid" },
+                                 { "header": "Definition",
                                    "tactic": "Wp.unfold", "params": {},
                                    "select": { "select": "clause-step",
                                                "at": 0, "kind": "have",
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
index 7088dae230bb076c156e35ba64b86218710ae268..81b6a3c63eaa995bcb9d50e5a03e1cff6e779fd4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
@@ -9,13 +9,6 @@
 ------------------------------------------------------------
 
 Goal Assertion (file unit_call.i, line 14):
-Assume {
-  Type: is_sint32(r_1) /\ is_sint32(r).
-  (* Call 'f' *)
-  Have: r < 0.
-  (* Call 'f' *)
-  Have: 0 < r_1.
-}
-Prove: r != r_1.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
index 96fd464c7d661aba8da4e1b6b8c8939905c3d33e..70022706b9fbae3ba71f400040391c85dd2f61ae 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
@@ -9,13 +9,6 @@
 ------------------------------------------------------------
 
 Goal Assertion (file unit_call.i, line 14):
-Assume {
-  Type: is_sint32(r_1) /\ is_sint32(r).
-  (* Call 'f' *)
-  Have: r < 0.
-  (* Call 'f' *)
-  Have: 0 < r_1.
-}
-Prove: r != r_1.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
index b8222c6a9e63711f4596018b136d7399ad70a120..c334ef3718ad2f469e9931a12cf58eab280775db 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
@@ -12,8 +12,6 @@ Goal Assertion 'OUT' (file unit_cast.i, line 5):
 unit_cast.i:4: warning from Typed Model:
  - Warning: Hide sub-term definition
    Reason: Cast with incompatible pointers types (source: sint32*) (target: sint8*)
-Let x = Mchar_0[w].
-Assume { Type: is_sint8(x). (* Heap *) Type: sconst(Mchar_0). }
-Prove: x <= 255.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
index 569fa012199a552edef54840ecb9189763856ed4..5d4f10b4737c1a8762185d5d66436e715bc2281d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
@@ -12,8 +12,6 @@ Goal Assertion 'OUT' (file unit_cast.i, line 5):
 unit_cast.i:4: warning from Typed Model:
  - Warning: Hide sub-term definition
    Reason: Cast with incompatible pointers types (source: sint32*) (target: sint8*)
-Let x = Mchar_0[w].
-Assume { Type: is_sint8(x). (* Heap *) Type: sconst(Mchar_0). }
-Prove: x <= 255.
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
index 4f262f161254f1b344217bfc2758b944c554031c..557801a559852a34dc42cbdb76461febdfc245a5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
@@ -51,24 +51,13 @@ Prove: x2_0 = v.
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 57)
 :
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 58)
 :
-Let m = p[k <- v].
-Assume {
-  Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
-      IsArray_sint32(m) /\ is_sint32(1 + k).
-  (* Pre-condition *)
-  Have: (0 <= k) /\ (k <= 8).
-  (* Call 'job' *)
-  Have: (k <= 9) /\ EqArray_int(10, m, p[k <- x1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -140,24 +129,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 70)
 :
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 71)
 :
-Let m = q[k <- v].
-Assume {
-  Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
-      is_sint32(1 + k).
-  (* Pre-condition *)
-  Have: (0 <= k) /\ (k <= 8).
-  (* Call 'job2' *)
-  Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -229,24 +207,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 83)
 :
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 84)
 :
-Let m = q[k <- v].
-Assume {
-  Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
-      is_sint32(1 + k).
-  (* Pre-condition *)
-  Have: (0 <= k) /\ (k <= 8).
-  (* Call 'job3' *)
-  Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
index a96c98731e45f72d2106339b9b9ca016604b8ded..0cc485057a91f86a7a1e48c1024cfe329cae413e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
@@ -51,24 +51,13 @@ Prove: x2_0 = v.
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 57)
 :
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 58)
 :
-Let m = p[k <- v].
-Assume {
-  Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
-      IsArray_sint32(m) /\ is_sint32(1 + k).
-  (* Pre-condition *)
-  Have: (0 <= k) /\ (k <= 8).
-  (* Call 'job' *)
-  Have: (k <= 9) /\ EqArray_int(10, m, p[k <- x1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -140,24 +129,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 70)
 :
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 71)
 :
-Let m = q[k <- v].
-Assume {
-  Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
-      is_sint32(1 + k).
-  (* Pre-condition *)
-  Have: (0 <= k) /\ (k <= 8).
-  (* Call 'job2' *)
-  Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -229,24 +207,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 83)
 :
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 84)
 :
-Let m = q[k <- v].
-Assume {
-  Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
-      is_sint32(1 + k).
-  (* Pre-condition *)
-  Have: (0 <= k) /\ (k <= 8).
-  (* Call 'job3' *)
-  Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
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 85d5372254429bead901a25a73e88c6565d6b25c..39e37a366cc59e64e9fe4893c56902f393af1c6e 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
@@ -68,24 +68,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'Range' (file user_init.i, line 16):
-Let a_1 = shift_sint32(a, 0).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: (region(a.base) <= 0) /\ linked(Malloc_0).
-  (* Pre-condition *)
-  Have: valid_rw(Malloc_0, a_1, n).
-  (* Invariant 'Range' *)
-  Have: 0 <= n.
-  (* Invariant 'Range' *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant 'Partial' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_1)] = v))).
-  (* Then *)
-  Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
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 2abe7e2f668fd269d0ed35cdab8c23f4125e9515..418fe8936dd4043f4655d28fc42f1a71cdbe472b 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
@@ -68,24 +68,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant 'Range' (file user_init.i, line 16):
-Let a_1 = shift_sint32(a, 0).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Heap *)
-  Type: (region(a.base) <= 0) /\ linked(Malloc_0).
-  (* Pre-condition *)
-  Have: valid_rw(Malloc_0, a_1, n).
-  (* Invariant 'Range' *)
-  Have: 0 <= n.
-  (* Invariant 'Range' *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant 'Partial' *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_1)] = v))).
-  (* Then *)
-  Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
index 409348e3f43cc5f6baf5e91d530c0238a2f03c19..a0ad9eb6560ad6a0eb083c7c994e98c4fab964e8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
@@ -45,27 +45,12 @@ Prove: L_fact(n) = F1_0.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file user_rec.i, line 15):
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i) /\
-      is_sint32(L_fact(i - 1)).
-  (* Else *)
-  Have: 2 <= n.
-  (* Invariant *)
-  Have: 0 < n.
-  (* Invariant *)
-  Have: L_fact(1) = 1.
-  (* Invariant *)
-  Have: (2 <= i) /\ (i <= (1 + n)).
-  (* Then *)
-  Have: i <= n.
-}
-Prove: 0 < i.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Establishment of Invariant (file user_rec.i, line 15):
-Assume { Type: is_sint32(n). (* Else *) Have: 2 <= n. }
-Prove: 0 < n.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -181,8 +166,7 @@ Prove: if (n <= 1) then (i = 1) else (0 < i).
 ------------------------------------------------------------
 
 Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 28):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -270,8 +254,7 @@ Prove: if (n <= 1) then (x_1 = n_1) else (n_1 <= x_1).
 ------------------------------------------------------------
 
 Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 41):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
index 56da8ae60125b5030fabb2fcc1b26daaae7c89fb..f5f40e3f1169944a0c2c8409db455eed6d2d053b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
@@ -45,27 +45,12 @@ Prove: L_fact(n) = F1_0.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file user_rec.i, line 15):
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i) /\
-      is_sint32(L_fact(i - 1)).
-  (* Else *)
-  Have: 2 <= n.
-  (* Invariant *)
-  Have: 0 < n.
-  (* Invariant *)
-  Have: L_fact(1) = 1.
-  (* Invariant *)
-  Have: (2 <= i) /\ (i <= (1 + n)).
-  (* Then *)
-  Have: i <= n.
-}
-Prove: 0 < i.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Establishment of Invariant (file user_rec.i, line 15):
-Assume { Type: is_sint32(n). (* Else *) Have: 2 <= n. }
-Prove: 0 < n.
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -181,8 +166,7 @@ Prove: if (n <= 1) then (i = 1) else (0 < i).
 ------------------------------------------------------------
 
 Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 28):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
 
 ------------------------------------------------------------
 
@@ -270,8 +254,7 @@ Prove: if (n <= 1) then (x_1 = n_1) else (n_1 <= x_1).
 ------------------------------------------------------------
 
 Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 41):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index 2389a4fcd586f975c134e67c237dafd499d11824..fbc663bb95acbeac2fcb60827b93d357b57d006a 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -41,24 +41,7 @@ Prove: Mint_0[shift_sint32(a, i)] = v[i].
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file caveat2.i, line 21):
-Assume {
-  Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
-  (* Pre-condition *)
-  Have: n <= 3.
-  Have: ({ Init_p_0 with Init_F1_S_n = true }) = Init_p_0.
-  (* Invariant *)
-  Have: 0 <= n.
-  (* Loop assigns ... *)
-  Have: ({ Init_p_0 with Init_F1_S_a = v }) = Init_p_0.
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= n).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (Mint_0[shift_sint32(global(G_b_26), i_1)] = v_1[i_1]))).
-  (* Then *)
-  Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------
 
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index 82c8bbe685e4f64775f367b669c89d585e07a23c..8411b76b58db2c71fdfa5e787b3a7c09794680cf 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -51,22 +51,7 @@ Prove: a_1[shiftfield_F1_S_g(shift_S1_S(a, i))] = 2.
 ------------------------------------------------------------
 
 Goal Preservation of Invariant (file caveat_range.i, line 19):
-Let a = global(G_p_22).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
-Assume {
-  Type: is_sint32(i) /\ is_sint32(1 + i).
-  (* Invariant *)
-  Have: (0 <= i) /\ (i <= 10).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_1))] = 1))).
-  (* Invariant *)
-  Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
-      (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_1))] = 2))).
-  (* Then *)
-  Have: i <= 9.
-}
-Prove: (-1) <= i.
+Prove: true.
 
 ------------------------------------------------------------