diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index 3d7d53107850aa94a02d58c623c27e413be03c38..4773e0b0310047318f83d07d7bdfeb0b2539356c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -33,6 +33,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -48,8 +49,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index 97118b6b366ae36a2de0da6a1e7fbba00070cc2e..ff529ac753db6af667533dbc84bc336486e806ee 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -25,6 +25,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -56,8 +57,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
index 8753ecac9cfde95f929c1100ba135fa644f94f84..5b143f91676c7f263265557b474ff4dcf2d3cbcb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle
@@ -25,9 +25,11 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [value] using specification for function __initialize
 tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
 [value] using specification for function __valid
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 4905c23b5c3158687a6e34a1aae7e206eb81e639..16b7e91901b0fd39c87ee5d7c745e1bedbfe6768 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -21,9 +21,11 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic functio
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [value] using specification for function __initialize
 tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid.
 [value] using specification for function __valid
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index feccbdb6ddb785f724c6161f27796d73f1476dc5..17c82b489881e72f95777fd4e8837b7956918ba0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -47,10 +47,10 @@ tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_4 < 10;
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
index 87104bf62ca34972a0952356156cb3f2dd9add59..2e97f3d935b6dde42b7bcb1dd6027f97f9123872 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle
@@ -25,6 +25,7 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -34,5 +35,6 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __initialize
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 50d22446a3ca7d28710ae0fa2b70ea3fca0a0d17..7bcb0d299272e897bb857a1ffc73892ee4b0a4b0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -21,6 +21,7 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun
   __memory_size ∈ [--..--]
 [value] using specification for function __store_block
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -30,5 +31,6 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __initialize
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
index 91c1eca5dae1dba97289607cf38cc60604e5ca79..56aa4ebae24aaf2e2853c8334206b779478ccd36 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle
@@ -40,6 +40,7 @@ tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -62,8 +63,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 0b1fb4930fbc4fb10a6e9b7512f80cc0d4af92c2..e45b62a3e03ea69d8c4d3348f388169bbd133c49 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -32,6 +32,7 @@ tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -54,8 +55,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
index 3abdd3f29587cf95fd9346b86d7033d9169a4eb9..e867ea1e46ba6b2b4259bd1ae885598c2dc5bf2c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle
@@ -37,6 +37,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -51,8 +52,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index 2fc23efb1a94f70d0863a4eafa42a3640a92a30a..250286e8054158bc0197beb7806654cd1c449c4c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -29,6 +29,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -49,8 +50,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid.
 tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
index 2fa35f293f36e4a511d99c978162b4ae02244ba7..a4d6c584761e714e906fbff5d7754489519c5866 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle
@@ -39,6 +39,7 @@ tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -51,8 +52,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 7d92075851e3a56b79160691ff03270018ff0e28..449c89e8f5ea578aa172378cb4285ad035500188 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -31,6 +31,7 @@ tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156
 [value] using specification for function __delete_block
 FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
@@ -50,8 +51,8 @@ FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior dealloca
 :0:[value] Assigning imprecise value to __e_acsl_implies.
         The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}
 FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies.
-        It contains a garbled mix of {Frama_C_alloc} because of Arithmetic
-        {FRAMAC_SHARE/libc/stdlib.h:178}.
+        It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of
+        Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}.
 FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main