From 311a5cd9b2f1d80a3aa3e157661fe4a8e0b17308 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 22 Sep 2021 11:05:08 +0200
Subject: [PATCH] [wp] Better management of trivial FALSE in the context in
 Condition.ml - do not drop type step without variables - better management of
 Branch/Either in Condition.ml

---
 src/plugins/wp/Conditions.ml                  |  34 +++---
 .../assigned_initialized_memtyped.res.oracle  |  14 ++-
 ...signed_not_initialized_memtyped.res.oracle |  23 +++-
 .../wp_acsl/oracle/block_length.res.oracle    |  56 +++++++--
 .../oracle/init_value_mem.0.res.oracle        |   4 +
 .../oracle/initialized_memtyped.res.oracle    |  12 +-
 .../wp/tests/wp_acsl/oracle/logic.res.oracle  |  21 ++++
 .../wp/tests/wp_acsl/oracle/null.res.oracle   |   4 +-
 .../tests/wp_acsl/oracle/pointer.res.oracle   |  53 ++++++--
 .../tests/wp_bts/oracle/bts_2079.res.oracle   |   6 +-
 .../tests/wp_plugin/oracle/flash.0.res.oracle | 114 ++++++++++--------
 .../tests/wp_plugin/oracle/flash.1.res.oracle | 108 ++++++++++-------
 .../oracle/init_const_guard.res.oracle        |   2 +-
 .../wp_plugin/oracle/overassign.res.oracle    |  16 +--
 .../tests/wp_store/oracle/struct.res.oracle   |   4 +
 .../wp_tip/oracle/chunk_printing.res.oracle   |   2 +-
 .../wp_typed/oracle/unit_hard.0.res.oracle    |   7 +-
 .../wp_typed/oracle/unit_hard.1.res.oracle    |   7 +-
 18 files changed, 334 insertions(+), 153 deletions(-)

diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index f7386b5cf3b..6f74f1dcde9 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -83,16 +83,16 @@ and sequence = {
   seq_vars : Vars.t ;
   seq_core : Pset.t ;
   seq_catg : category ;
-  seq_list : step list ;
+  seq_list : step list ; (* forall i . 0 <= i < n ==> Step_i *)
 }
 and condition =
-  | Type of pred
+  | Type of pred (* related to Type *)
   | Have of pred
-  | When of pred
+  | When of pred (* related to Condition *)
   | Core of pred
   | Init of pred
-  | Branch of pred * sequence * sequence
-  | Either of sequence list
+  | Branch of pred * sequence * sequence (* if Pred then Seq_1 else Seq_2 *)
+  | Either of sequence list (* exist i . 0 <= i < n && Sequence_i *)
   | State of Mstate.state
 
 (* -------------------------------------------------------------------------- *)
@@ -318,15 +318,19 @@ let pretty = ref (fun _fmt _seq -> ())
 
 let is_true = function { seq_catg = TRUE | EMPTY } -> true | _ -> false
 let is_empty = function { seq_catg = EMPTY } -> true | _ -> false
+let is_false = function { seq_catg = FALSE } -> true | _ -> false
 
 let is_absurd_h h = match h.condition with
-  | (Core p | When p | Have p) -> p == F.p_false
-  | _ -> false
+  | (Type p | Core p | When p | Have p | Init p) -> p == F.p_false
+  | Branch(_,p,q) -> is_false p && is_false q
+  | Either w -> List.for_all is_false w (* note: an empty w is an absurd hyp *)
+  | State _ -> false
 
 let is_trivial_h h = match h.condition with
   | State _ -> false
   | (Type p | Core p | When p | Have p | Init p) -> p == F.p_true
   | Branch(_,a,b) -> is_true a && is_true b
+  | Either [] -> false
   | Either w -> List.for_all is_true w
 
 let is_trivial_hs_p hs p = p == F.p_true || List.exists is_absurd_h hs
@@ -613,6 +617,7 @@ let core_branch step p a b =
   let condition =
     match a.seq_catg , b.seq_catg with
     | (TRUE | EMPTY) , (TRUE|EMPTY) -> Have p_true
+    | FALSE , FALSE -> Have p_false
     | _ -> Branch(p,a,b)
   in update_cond step condition
 
@@ -691,8 +696,9 @@ and map_steplist f = function
   | [] -> []
   | h::hs ->
       let h = map_step f h in
-      let hs = map_steplist f hs in
-      if is_trivial_h h then hs else h :: hs
+      if is_absurd_h h then [h] else
+        let hs = map_steplist f hs in
+        if is_trivial_h h then hs else h :: hs
 
 and map_sequence f s =
   sequence (map_steplist f s.seq_list)
@@ -736,8 +742,9 @@ and ground_flowdir ~fwd env = function
   | [] -> []
   | h::hs ->
       let h = ground_flow ~fwd env h in
-      let hs = ground_flowdir ~fwd env hs in
-      if is_trivial_h h then hs else h :: hs
+      if is_absurd_h h then [h] else
+        let hs = ground_flowdir ~fwd env hs in
+        if is_trivial_h h then hs else h :: hs
 
 let ground (hs,g) =
   let hs = ground_flowlist ~fwd:true (Ground.top ()) hs in
@@ -787,13 +794,12 @@ let letify_assume sref (_,step) =
           sref := Sigma.assume current p
   end ; current
 
-[@@@ warning "-32"]
 let rec letify_type sigma used p = match F.p_expr p with
   | And ps -> p_all (letify_type sigma used) ps
   | _ ->
       let p = Sigma.p_apply sigma p in
-      if Vars.intersect used (F.varsp p) then p else F.p_true
-[@@@ warning "+32"]
+      let vs = F.varsp p in
+      if Vars.intersect used vs || Vars.is_empty vs then p else F.p_true
 
 let rec letify_seq sigma0 ~target ~export (seq : step list) =
   let dseq = Array.map (dseq_of_step sigma0) (Array.of_list seq) in
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
index eb064ee4a7e..0b80f09a455 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
@@ -56,7 +56,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 126):
-Assume { (* Heap *) Type: cinits(Init_0). }
+Assume { (* Heap *) Type: (region(G_glob_82) <= 0) /\ cinits(Init_0). }
 Prove: IsInit_S1_S(global(G_glob_82), Init_0).
 
 ------------------------------------------------------------
@@ -68,7 +68,8 @@ Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(pg_0) <- true],
 Assume {
   Type: is_sint32(i) /\ is_sint32(1 + i).
   (* Heap *)
-  Type: (region(pg_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_82) <= 0) /\ (region(pg_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns 'CHECK' *)
   Have: cinits(a_1).
   (* Invariant 'CHECK' *)
@@ -97,7 +98,8 @@ Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
 Assume {
   Type: is_sint32(i) /\ is_sint32(i_1).
   (* Heap *)
-  Type: (region(pg_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_82) <= 0) /\ (region(pg_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns 'CHECK' *)
   Have: cinits(a_2).
   (* Invariant 'CHECK' *)
@@ -125,7 +127,8 @@ Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
 Assume {
   Type: is_sint32(i) /\ is_sint32(i_1).
   (* Heap *)
-  Type: (region(pg_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_82) <= 0) /\ (region(pg_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns 'CHECK' *)
   Have: cinits(a_2).
   (* Invariant 'CHECK' *)
@@ -178,7 +181,8 @@ Effect at line 139
 Assume {
   Type: is_sint32(i_1) /\ is_sint32(i).
   (* Heap *)
-  Type: (region(pg_0.base) <= 0) /\ linked(Malloc_0).
+  Type: (region(G_glob_82) <= 0) /\ (region(pg_0.base) <= 0) /\
+      linked(Malloc_0).
   (* Goal *)
   When: !invalid(Malloc_0, shift_sint32(shiftfield_F1_S_a(pg_0), i), 1).
   (* Invariant 'CHECK' *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
index c9c0e0bd127..605ed35e032 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
@@ -31,7 +31,8 @@ Let a_1 = havoc(Init_undef_0, a, shift_sint32(pg_array_0, 0), 10).
 Assume {
   Type: is_sint32(i).
   (* Heap *)
-  Type: (region(pg_array_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_array_51) <= 0) /\ (region(pg_array_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns ... *)
   Have: cinits(a) /\ cinits(a_1).
   (* Else *)
@@ -48,7 +49,8 @@ Let a_2 = havoc(Init_undef_0, a_1, shift_sint32(pg_array_0, 0), 10).
 Assume {
   Type: is_sint32(i).
   (* Heap *)
-  Type: (region(pg_array_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_array_51) <= 0) /\ (region(pg_array_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns ... *)
   Have: cinits(a_1) /\ cinits(a_2).
   (* Else *)
@@ -62,7 +64,13 @@ Prove: IsInitArray_sint32(a, 10, a_2).
 ------------------------------------------------------------
 
 Goal Check 'FAIL' (file tests/wp_acsl/assigned_not_initialized_memtyped.i, line 38):
-Assume { Type: is_sint32(i_1). (* Else *) Have: 10 <= i_1. }
+Assume {
+  Type: is_sint32(i_1).
+  (* Heap *)
+  Type: region(G_glob_atomic_39) <= 0.
+  (* Else *)
+  Have: 10 <= i_1.
+}
 Prove: (i=true).
 
 ------------------------------------------------------------
@@ -74,7 +82,8 @@ Let m_1 = m[pg_atomic_0 <- i_1].
 Assume {
   Type: is_sint32(i_2).
   (* Heap *)
-  Type: (region(pg_atomic_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_atomic_39) <= 0) /\ (region(pg_atomic_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns ... *)
   Have: cinits(m) /\ cinits(m_1).
   (* Else *)
@@ -93,7 +102,8 @@ Let a_1 = havoc(Init_undef_0, a, pg_comp_0, 11).
 Assume {
   Type: is_sint32(i).
   (* Heap *)
-  Type: (region(pg_comp_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_comp_45) <= 0) /\ (region(pg_comp_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns ... *)
   Have: cinits(a) /\ cinits(a_1).
   (* Else *)
@@ -110,7 +120,8 @@ Let a_2 = havoc(Init_undef_0, a_1, pg_comp_0, 11).
 Assume {
   Type: is_sint32(i).
   (* Heap *)
-  Type: (region(pg_comp_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_glob_comp_45) <= 0) /\ (region(pg_comp_0.base) <= 0) /\
+      cinits(Init_0).
   (* Loop assigns ... *)
   Have: cinits(a_1) /\ cinits(a_2).
   (* Else *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle
index 65ef2d0c10a..82a11829eac 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle
@@ -60,7 +60,12 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'Pt' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: (Malloc_0[G_t_20] / 20) = 1.
 
 ------------------------------------------------------------
@@ -71,7 +76,12 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'Pmat1' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: (Malloc_0[G_mat_21] / 5) = 10.
 
 ------------------------------------------------------------
@@ -82,37 +92,67 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'Pmat2' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: (Malloc_0[G_mat_21] / 50) = 1.
 
 ------------------------------------------------------------
 
 Goal Post-condition 'Ps' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: (4 + Malloc_0[G_x_22]) = (5 * (Malloc_0[G_s_23] / 5)).
 
 ------------------------------------------------------------
 
 Goal Post-condition 'Pts' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: (Malloc_0[G_ts_24] / 20) = (Malloc_0[G_s_23] / 5).
 
 ------------------------------------------------------------
 
 Goal Post-condition 'Pt1' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: Malloc_0[G_t_20] = 20.
 
 ------------------------------------------------------------
 
 Goal Post-condition 'Pmat12' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: Malloc_0[G_mat_21] = 50.
 
 ------------------------------------------------------------
 
 Goal Post-condition 'Pts1' in 'g':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_mat_21) <= 0) /\ (region(G_s_23) <= 0) /\
+      (region(G_t_20) <= 0) /\ (region(G_ts_24) <= 0) /\
+      (region(G_x_22) <= 0) /\ linked(Malloc_0).
+}
 Prove: (Malloc_0[G_ts_24] / 5) = (4 * (Malloc_0[G_s_23] / 5)).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
index c1cd26ad017..568bd1a211c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
@@ -11,6 +11,8 @@ Let a = global(G_v_20).
 Let a_1 = Load_S1_St(a, Mint_0).
 Assume {
   Type: IsS1_St(w) /\ IsS1_St(a_1).
+  (* Heap *)
+  Type: region(G_v_20) <= 0.
   (* Initializer *)
   Init: (w.F1_St_a) = 1.
   (* Initializer *)
@@ -29,6 +31,8 @@ Let a = global(G_v_20).
 Let a_1 = Load_S1_St(a, Mint_0).
 Assume {
   Type: IsS1_St(w) /\ IsS1_St(a_1).
+  (* Heap *)
+  Type: region(G_v_20) <= 0.
   (* Initializer *)
   Init: (w.F1_St_a) = 1.
   (* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
index ef64e214217..639dbc2fcbd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
@@ -18,7 +18,7 @@ Prove: (Init_0[global(P_x_59)]=true).
 Goal Post-condition 'provable' in 'glob_arr':
 Assume {
   (* Heap *)
-  Type: cinits(Init_0).
+  Type: (region(G_ga_47) <= 0) /\ cinits(Init_0).
   (* Goal *)
   When: (0 <= i) /\ (i <= 4).
 }
@@ -29,7 +29,8 @@ Prove: (Init_0[shift_sint32(global(G_ga_47), i)]=true).
 Goal Post-condition 'unknown' in 'glob_arr':
 Assume {
   (* Heap *)
-  Type: (region(pga_0.base) <= 0) /\ cinits(Init_0).
+  Type: (region(G_ga_47) <= 0) /\ (region(pga_0.base) <= 0) /\
+      cinits(Init_0).
   (* Goal *)
   When: (0 <= i) /\ (i <= 4).
 }
@@ -41,13 +42,16 @@ Prove: (Init_0[shift_sint32(pga_0, i)]=true).
 ------------------------------------------------------------
 
 Goal Post-condition 'provable' in 'glob_var':
-Assume { (* Heap *) Type: cinits(Init_0). }
+Assume { (* Heap *) Type: (region(G_gx_41) <= 0) /\ cinits(Init_0). }
 Prove: (Init_0[global(G_gx_41)]=true).
 
 ------------------------------------------------------------
 
 Goal Post-condition 'unknown' in 'glob_var':
-Assume { (* Heap *) Type: (region(px_0.base) <= 0) /\ cinits(Init_0). }
+Assume {
+  (* Heap *)
+  Type: (region(G_gx_41) <= 0) /\ (region(px_0.base) <= 0) /\ cinits(Init_0).
+}
 Prove: (Init_0[px_0]=true).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index 84f53ddd896..d433485267e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -73,6 +73,8 @@ Let a_3 = shift_S1(a, 0).
 Let m = Array_S1(a, 3, Mint_0).
 Assume {
   Type: IsArray_S1(m) /\ IsArray_S1(Array_S1(a_3, 3, Mint_0)).
+  (* Heap *)
+  Type: region(G_tr_35) <= 0.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
@@ -98,6 +100,8 @@ Let a_3 = shift_S1(a, 0).
 Let m = Array_S1(a, 3, Mint_0).
 Assume {
   Type: IsArray_S1(m) /\ IsArray_S1(Array_S1(a_3, 3, Mint_0)).
+  (* Heap *)
+  Type: region(G_tr_35) <= 0.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
@@ -123,6 +127,8 @@ Let a_3 = shift_S1(a, 0).
 Let m = Array_S1(a_3, 3, Mint_0).
 Assume {
   Type: IsArray_S1(Array_S1(a, 3, Mint_0)) /\ IsArray_S1(m).
+  (* Heap *)
+  Type: region(G_tr_35) <= 0.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
   (* Initializer *)
@@ -144,6 +150,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:49: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Tint2) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: (w.F1_y) = 11.
 
 ------------------------------------------------------------
@@ -152,6 +159,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:50: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Point) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: (w.F3_tab)[1] = 11.
 
 ------------------------------------------------------------
@@ -160,6 +168,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:51: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast to struct (Point) from (int [2]) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: (w.F1_y) = 11.
 
 ------------------------------------------------------------
@@ -168,6 +177,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:52: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Point) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: w[1] = 11.
 
 ------------------------------------------------------------
@@ -176,6 +186,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:53: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Tint2) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: w[1] = 11.
 
 ------------------------------------------------------------
@@ -184,6 +195,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:54: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Buint) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: w = 134480385.
 
 ------------------------------------------------------------
@@ -197,6 +209,8 @@ Let a_1 = shiftfield_F4_bytes(a).
 Let a_2 = Load_S4(a, Mint_0).
 Assume {
   Type: IsS4(a_2).
+  (* Heap *)
+  Type: region(G_tr_35) <= 0.
   (* Initializer *)
   Init: Mint_0[shift_uint8(a_1, 0)] = 1.
   (* Initializer *)
@@ -214,6 +228,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:56: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Tint6) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: (w[1].F1_y) = 21.
 
 ------------------------------------------------------------
@@ -222,6 +237,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:57: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast to sized array (Triangle) from (int [6]) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: (w[1].F1_y) = 21.
 
 ------------------------------------------------------------
@@ -230,6 +246,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:58: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Tint6) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: w[4] = 30.
 
 ------------------------------------------------------------
@@ -238,6 +255,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:59: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Tint6) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: w[1] = 11.
 
 ------------------------------------------------------------
@@ -246,6 +264,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:60: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast to sized array (int [2]) from (int [6]) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: w[1] = 11.
 
 ------------------------------------------------------------
@@ -254,6 +273,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:61: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast from struct (Tint6) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: (w.F3_tab)[1] = 11.
 
 ------------------------------------------------------------
@@ -262,6 +282,7 @@ Goal Pre-condition 'qed_ok' in 'main':
 tests/wp_acsl/logic.i:62: warning from wp:
  - Warning: Hide sub-term definition
    Reason: Logic cast to struct (Tint2) from (int [6]) not implemented yet
+Assume { (* Heap *) Type: region(G_tr_35) <= 0. }
 Prove: (w.F3_tab)[1] = 11.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
index 00b77b3dcea..0157e50fb50 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
@@ -43,14 +43,14 @@ Prove: true.
 
 Goal Assigns nothing in 'prover':
 Call Effect at line 32
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(L_GET.base) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, L_GET, 1).
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'prover':
 Call Effect at line 32
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(L_GET.base) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, L_GET, 1).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
index e261e262d43..e35b6c6314b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
@@ -21,7 +21,7 @@
 Goal Post-condition 'qed_ko,Base_oracle_ko' in 'absurd':
 Assume {
   (* Heap *)
-  Type: region(q.base) <= 0.
+  Type: (region(G_t_21) <= 0) /\ (region(q.base) <= 0).
   (* Goal *)
   When: q.offset < p.offset.
   (* Pre-condition *)
@@ -33,6 +33,8 @@ Prove: addr_lt(q, p).
 
 Goal Post-condition 'qed_ko,Comp_oracle_ko' in 'absurd':
 Assume {
+  (* Heap *)
+  Type: region(G_t_21) <= 0.
   (* Goal *)
   When: i_1 <= i.
   (* Pre-condition *)
@@ -115,7 +117,14 @@ Goal Post-condition 'qed_ok,Lt' in 'mixed_array_pointer':
 tests/wp_acsl/pointer.i:45: warning from Reference Variable Model:
  - Warning: Hide sub-term definition
    Reason: Uncomparable locations p_0 and mem:t.(0)
-Assume { (* Goal *) When: 0 < w. (* Pre-condition *) Have: p.base = G_t_21. }
+Assume {
+  (* Heap *)
+  Type: region(G_t_21) <= 0.
+  (* Goal *)
+  When: 0 < w.
+  (* Pre-condition *)
+  Have: p.base = G_t_21.
+}
 Prove: addr_lt(shift_sint32(global(G_t_21), 0), p).
 
 ------------------------------------------------------------
@@ -124,7 +133,13 @@ Goal Post-condition 'qed_ok,Le' in 'mixed_array_pointer':
 tests/wp_acsl/pointer.i:46: warning from Reference Variable Model:
  - Warning: Hide sub-term definition
    Reason: Uncomparable locations p_0 and mem:t.(0)
-Assume { (* Goal *) When: 0 <= w. (* Pre-condition *) Have: p.base = G_t_21.
+Assume {
+  (* Heap *)
+  Type: region(G_t_21) <= 0.
+  (* Goal *)
+  When: 0 <= w.
+  (* Pre-condition *)
+  Have: p.base = G_t_21.
 }
 Prove: addr_le(shift_sint32(global(G_t_21), 0), p).
 
@@ -134,7 +149,12 @@ Goal Post-condition 'qed_ok,Eq' in 'mixed_array_pointer':
 tests/wp_acsl/pointer.i:47: warning from Reference Variable Model:
  - Warning: Hide sub-term definition
    Reason: Uncomparable locations p_0 and mem:t.(0)
-Assume { (* Pre-condition *) Have: p.base = G_t_21. }
+Assume {
+  (* Heap *)
+  Type: region(G_t_21) <= 0.
+  (* Pre-condition *)
+  Have: p.base = G_t_21.
+}
 Prove: shift_sint32(global(G_t_21), 0) = p.
 
 ------------------------------------------------------------
@@ -143,7 +163,13 @@ Goal Post-condition 'qed_ok,Ne' in 'mixed_array_pointer':
 tests/wp_acsl/pointer.i:48: warning from Reference Variable Model:
  - Warning: Hide sub-term definition
    Reason: Uncomparable locations p_0 and mem:t.(0)
-Assume { (* Goal *) When: w != 0. (* Pre-condition *) Have: p.base = G_t_21.
+Assume {
+  (* Heap *)
+  Type: region(G_t_21) <= 0.
+  (* Goal *)
+  When: w != 0.
+  (* Pre-condition *)
+  Have: p.base = G_t_21.
 }
 Prove: shift_sint32(global(G_t_21), 0) != p.
 
@@ -153,7 +179,13 @@ Goal Post-condition 'qed_ko,Le_oracle_ko' in 'mixed_array_pointer':
 tests/wp_acsl/pointer.i:49: warning from Reference Variable Model:
  - Warning: Hide sub-term definition
    Reason: Uncomparable locations p_0 and mem:t.(0)
-Assume { (* Goal *) When: 0 <= w. (* Pre-condition *) Have: p.base = G_t_21.
+Assume {
+  (* Heap *)
+  Type: region(G_t_21) <= 0.
+  (* Goal *)
+  When: 0 <= w.
+  (* Pre-condition *)
+  Have: p.base = G_t_21.
 }
 Prove: addr_lt(shift_sint32(global(G_t_21), 0), p).
 
@@ -163,7 +195,14 @@ Goal Post-condition 'qed_ko,Lt_oracle_ko' in 'mixed_array_pointer':
 tests/wp_acsl/pointer.i:50: warning from Reference Variable Model:
  - Warning: Hide sub-term definition
    Reason: Uncomparable locations p_0 and mem:t.(0)
-Assume { (* Goal *) When: 0 < w. (* Pre-condition *) Have: p.base = G_t_21. }
+Assume {
+  (* Heap *)
+  Type: region(G_t_21) <= 0.
+  (* Goal *)
+  When: 0 < w.
+  (* Pre-condition *)
+  Have: p.base = G_t_21.
+}
 Prove: addr_le(p, shift_sint32(global(G_t_21), 0)).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle
index a59bf702249..9be0aa541fc 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle
@@ -7,19 +7,19 @@
 ------------------------------------------------------------
 
 Goal Post-condition 'Obs,P' in 'main':
-Assume { Type: is_sint32(k). }
+Assume { Type: is_sint32(k). (* Heap *) Type: region(0) <= 0. }
 Prove: P_S(k).
 
 ------------------------------------------------------------
 
 Goal Post-condition 'Obs,Q' in 'main':
-Assume { Type: is_sint32(k). }
+Assume { Type: is_sint32(k). (* Heap *) Type: region(0) <= 0. }
 Prove: P_S(k).
 
 ------------------------------------------------------------
 
 Goal Post-condition 'Obs,R' in 'main':
-Assume { Type: is_sint32(k). }
+Assume { Type: is_sint32(k). (* Heap *) Type: region(0) <= 0. }
 Prove: P_S(45 + k).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
index f10a2975696..8d643dca787 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
@@ -27,24 +27,28 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 1.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 2.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, L_RD_access(L_INDEX_init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, L_RD_access(a_8, a_2)).
+Let x_8 = RD_time_0 - 2.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, L_RD_access(a_5, a_2)).
+Let x_11 = L_RD_value(a, L_RD_access(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
-      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
-      is_sint32(x_1) /\ is_sint32(x_2).
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
+      is_sint32(x_8) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_6) /\
+      is_sint32(x_10) /\ is_sint32(x_11) /\ is_sint32(x_7) /\
+      is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = L_INDEX_init.
+  Have: L_RD_current(x_8) = L_INDEX_init.
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
-        + L_RD_value(a_2, L_RD_access(a_8, a_2)))
-         = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
+      (x_7 = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -74,24 +78,28 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 1.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 2.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, L_RD_access(L_INDEX_init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, L_RD_access(a_8, a_2)).
+Let x_8 = RD_time_0 - 2.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, L_RD_access(a_5, a_2)).
+Let x_11 = L_RD_value(a, L_RD_access(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
-      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
-      is_sint32(x_1) /\ is_sint32(x_2).
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
+      is_sint32(x_8) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_6) /\
+      is_sint32(x_10) /\ is_sint32(x_11) /\ is_sint32(x_7) /\
+      is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = L_INDEX_init.
+  Have: L_RD_current(x_8) = L_INDEX_init.
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
-        + L_RD_value(a_2, L_RD_access(a_8, a_2)))
-         = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
+      (x_7 = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -121,24 +129,27 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 2.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 3.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, L_RD_access(L_INDEX_init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, L_RD_access(a_8, a_2)).
+Let x_8 = RD_time_0 - 3.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, L_RD_access(a_5, a_2)).
+Let x_11 = L_RD_value(a, L_RD_access(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1).
+      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
+      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = L_INDEX_init.
+  Have: L_RD_current(x_8) = L_INDEX_init.
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_8) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
-        + L_RD_value(a_2, L_RD_access(a_8, a_2)))
-         = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
+      (x_7 = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -168,23 +179,27 @@ Let x_4 = RD_time_0 - 2.
 Let a_7 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
 Let x_6 = L_RD_value(a, L_RD_access(L_INDEX_init, a)).
-Let x_7 = RD_time_0 - 3.
-Let x_8 = OBSERVER_time_0 - 3.
+Let x_7 = x_6 + L_RD_value(a_2, L_RD_access(a_7, a_2)).
+Let x_8 = RD_time_0 - 3.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, L_RD_access(a_5, a_2)).
+Let x_11 = L_RD_value(a, L_RD_access(a_6, a)).
+Let x_12 = x_6 + x_10 + x_11.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_8) /\ is_sint32(x_7) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1).
+      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
+      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_12).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_8) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_7) = L_INDEX_init.
+  Have: L_RD_current(x_8) = L_INDEX_init.
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((x_6 + L_RD_value(a_2, L_RD_access(a_7, a_2)))
-         = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
+      (x_7 = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -194,9 +209,7 @@ Assume {
   Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
       (L_RD_update(a_6, a) = L_RD_current(RD_time_0)).
 }
-Prove: (x_6 + L_RD_value(a_2, L_RD_access(a_5, a_2))
-        + L_RD_value(a, L_RD_access(a_6, a)))
-         = (L_RD_value(a, 0) + L_RD_value(a, 1) + L_RD_value(a_2, 0)).
+Prove: x_12 = (L_RD_value(a, 0) + L_RD_value(a, 1) + L_RD_value(a_2, 0)).
 
 ------------------------------------------------------------
 
@@ -215,24 +228,27 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 2.
 Let a_7 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 3.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, L_RD_access(L_INDEX_init, a)).
+Let x_7 = x_6 + L_RD_value(a_2, L_RD_access(a_7, a_2)).
+Let x_8 = RD_time_0 - 3.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, L_RD_access(a_5, a_2)).
+Let x_11 = L_RD_value(a, L_RD_access(a_6, a)).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1).
+      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
+      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = L_INDEX_init.
+  Have: L_RD_current(x_8) = L_INDEX_init.
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = L_INDEX_init.
   (* Call 'RD' *)
   Have: (a_5 = a_7) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, L_RD_access(L_INDEX_init, a))
-        + L_RD_value(a_2, L_RD_access(a_7, a_2)))
-         = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
+      (x_7 = L_WR_value(a_2, L_WR_access(L_INDEX_init, a_2))).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
index c950a9aa736..ad702a82a85 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
@@ -29,23 +29,28 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 1.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 2.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, (const(0))[a]).
+Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
+Let x_8 = RD_time_0 - 2.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
+Let x_11 = L_RD_value(a, (a_6)[a]).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
-      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
-      is_sint32(x_1) /\ is_sint32(x_2).
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
+      is_sint32(x_8) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_6) /\
+      is_sint32(x_10) /\ is_sint32(x_11) /\ is_sint32(x_7) /\
+      is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = const(0).
+  Have: L_RD_current(x_8) = const(0).
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
-         = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -75,23 +80,28 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 1.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 2.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, (const(0))[a]).
+Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
+Let x_8 = RD_time_0 - 2.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
+Let x_11 = L_RD_value(a, (a_6)[a]).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_5) /\
-      is_sint32(x_6) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
-      is_sint32(x_1) /\ is_sint32(x_2).
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
+      is_sint32(x_8) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
+      is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_6) /\
+      is_sint32(x_10) /\ is_sint32(x_11) /\ is_sint32(x_7) /\
+      is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = const(0).
+  Have: L_RD_current(x_8) = const(0).
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
-         = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -121,23 +131,27 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 2.
 Let a_8 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 3.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, (const(0))[a]).
+Let x_7 = x_6 + L_RD_value(a_2, (a_8)[a_2]).
+Let x_8 = RD_time_0 - 3.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
+Let x_11 = L_RD_value(a, (a_6)[a]).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1).
+      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
+      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = const(0).
+  Have: L_RD_current(x_8) = const(0).
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_8)[a_2]))
-         = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -167,22 +181,27 @@ Let x_4 = RD_time_0 - 2.
 Let a_7 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
 Let x_6 = L_RD_value(a, (const(0))[a]).
-Let x_7 = RD_time_0 - 3.
-Let x_8 = OBSERVER_time_0 - 3.
+Let x_7 = x_6 + L_RD_value(a_2, (a_7)[a_2]).
+Let x_8 = RD_time_0 - 3.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
+Let x_11 = L_RD_value(a, (a_6)[a]).
+Let x_12 = x_6 + x_10 + x_11.
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_8) /\ is_sint32(x_7) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1).
+      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
+      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_12).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_8) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_7) = const(0).
+  Have: L_RD_current(x_8) = const(0).
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((x_6 + L_RD_value(a_2, (a_7)[a_2])) = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
@@ -192,8 +211,7 @@ Assume {
   Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
       (((a_6)[(a) <- (a_6)[a]+1]) = L_RD_current(RD_time_0)).
 }
-Prove: (x_6 + L_RD_value(a_2, (a_5)[a_2]) + L_RD_value(a, (a_6)[a]))
-         = (L_RD_value(a, 0) + L_RD_value(a, 1) + L_RD_value(a_2, 0)).
+Prove: x_12 = (L_RD_value(a, 0) + L_RD_value(a, 1) + L_RD_value(a_2, 0)).
 
 ------------------------------------------------------------
 
@@ -212,23 +230,27 @@ Let x_3 = OBSERVER_time_0 - 1.
 Let x_4 = RD_time_0 - 2.
 Let a_7 = L_RD_current(x_4).
 Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = RD_time_0 - 3.
-Let x_7 = OBSERVER_time_0 - 3.
+Let x_6 = L_RD_value(a, (const(0))[a]).
+Let x_7 = x_6 + L_RD_value(a_2, (a_7)[a_2]).
+Let x_8 = RD_time_0 - 3.
+Let x_9 = OBSERVER_time_0 - 3.
+Let x_10 = L_RD_value(a_2, (a_5)[a_2]).
+Let x_11 = L_RD_value(a, (a_6)[a]).
 Assume {
   Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_7) /\ is_sint32(x_6) /\
+      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
       is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1).
+      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
+      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_6 + x_10 + x_11).
   (* Pre-condition *)
-  Have: L_OBSERVER(x_7) = nil.
+  Have: L_OBSERVER(x_9) = nil.
   (* Pre-condition *)
-  Have: L_RD_current(x_6) = const(0).
+  Have: L_RD_current(x_8) = const(0).
   (* Pre-condition *)
   Have: L_WR_current(WR_time_0) = const(0).
   (* Call 'RD' *)
   Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      ((L_RD_value(a, (const(0))[a]) + L_RD_value(a_2, (a_7)[a_2]))
-         = L_WR_value(a_2, (const(0))[a_2])).
+      (x_7 = L_WR_value(a_2, (const(0))[a_2])).
   (* Call 'RD' *)
   Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
   (* Call 'WR' *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle
index 1b028ec86ba..090919a8e0d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle
@@ -12,7 +12,7 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'Pointed_Valid' in 'f':
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_x_20) <= 0) /\ linked(Malloc_0). }
 Prove: valid_rw(Malloc_0, global(G_x_20), 1).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
index 07bb9ac0b9f..41a487a1ca6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
@@ -38,14 +38,14 @@ Prove: true.
 
 Goal Assigns nothing in 'f3_ok':
 Call Effect at line 20
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), 20), 10).
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'f3_ok':
 Call Effect at line 20
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), 20), 10).
 
 ------------------------------------------------------------
@@ -55,14 +55,14 @@ Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), 20), 10).
 
 Goal Assigns nothing in 'f4_ok':
 Call Effect at line 23
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -10), 10).
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'f4_ok':
 Call Effect at line 23
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -10), 10).
 
 ------------------------------------------------------------
@@ -72,14 +72,14 @@ Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -10), 10).
 
 Goal Assigns nothing in 'f5_ko':
 Call Effect at line 26
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), 15), 10).
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'f5_ko':
 Call Effect at line 26
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), 15), 10).
 
 ------------------------------------------------------------
@@ -89,14 +89,14 @@ Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), 15), 10).
 
 Goal Assigns nothing in 'f6_ko':
 Call Effect at line 29
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -5), 10).
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'f6_ko':
 Call Effect at line 29
-Assume { (* Heap *) Type: linked(Malloc_0). }
+Assume { (* Heap *) Type: (region(G_A_32) <= 0) /\ linked(Malloc_0). }
 Prove: invalid(Malloc_0, shift_sint32(global(G_A_32), -5), 10).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
index 175f393e79e..a2d7febc52f 100644
--- a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
@@ -46,6 +46,8 @@ Let a = global(G_v_30).
 Let a_1 = Load_S2_St(a, Mint_0).
 Assume {
   Type: IsS2_St(w) /\ IsS2_St(a_1).
+  (* Heap *)
+  Type: region(G_v_30) <= 0.
   (* Initializer *)
   Init: (w.F2_St_a) = 1.
   (* Initializer *)
@@ -64,6 +66,8 @@ Let a = global(G_v_30).
 Let a_1 = Load_S2_St(a, Mint_0).
 Assume {
   Type: IsS2_St(w) /\ IsS2_St(a_1).
+  (* Heap *)
+  Type: region(G_v_30) <= 0.
   (* Initializer *)
   Init: (w.F2_St_a) = 1.
   (* Initializer *)
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index 598ec02c22b..5e34e7f660f 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -13,7 +13,7 @@ Assume {
   Type: is_sint32_chunk(µ:Msint32@L1) /\ is_uint32_chunk(µ:Muint32@L1) /\
       is_uint32(`x_1) /\ is_sint32(`x_2).
   (* Heap *)
-  Type: framed(µ:Mptr@L1).
+  Type: (region(0) <= 0) /\ framed(µ:Mptr@L1).
   Stmt { L1:  }
   Stmt { x.a = `v;  }
   (* Call 'get_int' *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle
index 8c6dba5f1eb..835328fb267 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle
@@ -17,6 +17,11 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Pre-condition 'r_is_q1_ko' in 'main':
-Prove: shift_sint32(addr_of_int(26352), 1) = addr_of_int(26360).
+Let a = addr_of_int(26352).
+Assume {
+  (* Heap *)
+  Type: (region(addr_of_int(13311).base) <= 0) /\ (region(a.base) <= 0).
+}
+Prove: shift_sint32(a, 1) = addr_of_int(26360).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle
index dc71a1a475c..039f899643d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle
@@ -17,6 +17,11 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Pre-condition 'r_is_q1_ko' in 'main':
-Prove: shift_sint32(addr_of_int(26352), 1) = addr_of_int(26360).
+Let a = addr_of_int(26352).
+Assume {
+  (* Heap *)
+  Type: (region(addr_of_int(13311).base) <= 0) /\ (region(a.base) <= 0).
+}
+Prove: shift_sint32(a, 1) = addr_of_int(26360).
 
 ------------------------------------------------------------
-- 
GitLab