diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
index 436b0b25bccda83473908c41a960a977fff56a72..fcc2455baeae82ac1722ad99c3f67407b3584eb2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
@@ -17,13 +17,15 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_acsl/base_offset.i, line 15) in 'f':
-Let x = p.offset.
+Let x = p.base.
+Let x_1 = base_offset_table(x).
+Let x_2 = p.offset.
 Assume {
   (* Heap *)
-  Type: region(p.base) <= 0.
+  Type: region(x) <= 0.
   (* Goal *)
   When: (0 <= i) /\ (i <= i_1) /\ (i_1 <= 3).
 }
-Prove: base_offset(1 + i + x) <= base_offset(1 + i_1 + x).
+Prove: base_offset(x_1, 1 + i + x_2) <= base_offset(x_1, 1 + i_1 + x_2).
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
index a8fdef13518b119b2286cdcee6d108108ea227e0..8b29211f4ecea61d71ded5c45410d36fc265b4fb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle
@@ -5,11 +5,11 @@
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_f_ensures : Valid
 [wp] [Qed] Goal typed_f_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_f_ensures_3 : Unsuccess
-[wp] Proved goals:    2 / 3
+[wp] [Alt-Ergo] Goal typed_f_ensures_3 : Valid
+[wp] Proved goals:    3 / 3
   Qed:             2 
-  Alt-Ergo:        0  (unsuccess: 1)
+  Alt-Ergo:        1
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  f                         2        -        3      66.7%
+  f                         2        1        3       100%
 ------------------------------------------------------------