diff --git a/src/plugins/e-acsl/tests/memory/init_function.c b/src/plugins/e-acsl/tests/memory/init_function.c
index 133c99f201d3abf69712aa1ea43009fa053e69eb..0b6f90eb08609a76dab8f5247e47003ebe553129 100644
--- a/src/plugins/e-acsl/tests/memory/init_function.c
+++ b/src/plugins/e-acsl/tests/memory/init_function.c
@@ -1,13 +1,19 @@
 /* run.config
-  COMMENT: Check if the instrumentation engine still adds __e_acsl_memory init
-  COMMENT: is inserted for the case when no malloc is used but no no variable
-  COMMENT: is required tracking
+  COMMENT: Check that the instrumentation engine still adds __e_acsl_memory_init
+  COMMENT: if no variable is instrumented.
+  STDOPT: +"-eva-no-builtins-auto"
 */
 
 #include <stdlib.h>
 
+extern size_t __e_acsl_heap_allocation_size;
+
 int main(void) {
-    /* @assert (__heap_allocation_size == 0);  */
-    char *a = malloc(7);
-    /* @assert (__heap_allocation_size == 7);  */
+  // The asserts check that the memory model of E-ACSL is correctly initialized
+  // and updated, but since no memory predicate is used the variable `a` does
+  // not need to be instrumented (ie. no `store_block` and `delete_block` are
+  // generated).
+  /*@ assert __e_acsl_heap_allocation_size == 0;  */
+  char *a = malloc(7);
+  /*@ assert __e_acsl_heap_allocation_size == 7;  */
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
index 7a579dc32d3c6c660a14d042948f8dc16e2191e1..0f80a70efb16cce469924cd3c6bd384fcabe2ec0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
@@ -4,11 +4,21 @@
 #include "stdlib.h"
 extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
+extern size_t __e_acsl_heap_allocation_size;
+
 int main(void)
 {
   int __retres;
   __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  __e_acsl_assert(__e_acsl_heap_allocation_size == 0UL,1,"Assertion","main",
+                  "__e_acsl_heap_allocation_size == 0",
+                  "tests/memory/init_function.c",16);
+  /*@ assert __e_acsl_heap_allocation_size ≡ 0; */ ;
   char *a = malloc((unsigned long)7);
+  __e_acsl_assert(__e_acsl_heap_allocation_size == 7UL,1,"Assertion","main",
+                  "__e_acsl_heap_allocation_size == 7",
+                  "tests/memory/init_function.c",18);
+  /*@ assert __e_acsl_heap_allocation_size ≡ 7; */ ;
   __retres = 0;
   __e_acsl_memory_clean();
   return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
index efd026311297e55d8fefb674326118e6ece88624..f8f3e0f93f7a84a7f02c488b6a9b4443fbea3b33 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
@@ -1,2 +1,12 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/memory/init_function.c:16: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/init_function.c:16: Warning: 
+  assertion got status unknown.
+[eva] tests/memory/init_function.c:17: Warning: 
+  ignoring unsupported \allocates clause
+[eva:alarm] tests/memory/init_function.c:18: Warning: 
+  function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/memory/init_function.c:18: Warning: 
+  assertion got status unknown.