diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index 9f336692a29ff1b5a71906f01a81e8137fda68b5..48ad882af35395630ea4e752ac3fbf7fdbbb5648 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -119,14 +119,16 @@ void f(void)
 
 void g(int *C, int *D)
 {
-  __store_block((void *)(& C),4U);
-  __full_init((void *)(& C));
-  __store_block((void *)(& D),4U);
-  __full_init((void *)(& D));
-  __full_init((void *)(& C));
-  C = D;
+  /*@ assert \initialized(&C); */
+  {
+    int __e_acsl_initialized;
+    __store_block((void *)(& C),4U);
+    __full_init((void *)(& C));
+    __e_acsl_initialized = __initialized((void *)(& C),sizeof(int *));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"g",
+                  (char *)"\\initialized(&C)",19);
+  }
   __delete_block((void *)(& C));
-  __delete_block((void *)(& D));
   return;
 }
 
@@ -144,51 +146,34 @@ int main(void)
   int __retres;
   int *x;
   int *y;
-  int *z;
-  int *t;
   e_acsl_global_init();
-  __store_block((void *)(& t),4U);
-  __store_block((void *)(& z),4U);
   __store_block((void *)(& y),4U);
   __store_block((void *)(& x),4U);
   __full_init((void *)(& B));
   B = (int *)__e_acsl_malloc(sizeof(int));
   __full_init((void *)(& y));
   y = (int *)__e_acsl_malloc(sizeof(int));
-  __full_init((void *)(& t));
-  t = (int *)__e_acsl_malloc(sizeof(int));
   __full_init((void *)(& x));
   x = y;
   f();
-  __full_init((void *)(& z));
-  __full_init((void *)(& t));
-  g(z,t);
   /*@ assert \initialized(&A); */
   {
     int __e_acsl_initialized;
     __e_acsl_initialized = __initialized((void *)(& A),sizeof(int *));
     e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&A)",30);
+                  (char *)"\\initialized(&A)",28);
   }
   /*@ assert \initialized(&x); */
   {
     int __e_acsl_initialized_2;
     __e_acsl_initialized_2 = __initialized((void *)(& x),sizeof(int *));
     e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&x)",31);
-  }
-  /*@ assert \initialized(&z); */
-  {
-    int __e_acsl_initialized_3;
-    __e_acsl_initialized_3 = __initialized((void *)(& z),sizeof(int *));
-    e_acsl_assert(__e_acsl_initialized_3,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&z)",32);
+                  (char *)"\\initialized(&x)",29);
   }
+  g(x,y);
   __retres = 0;
   __delete_block((void *)(& B));
   __delete_block((void *)(& A));
-  __delete_block((void *)(& t));
-  __delete_block((void *)(& z));
   __delete_block((void *)(& y));
   __delete_block((void *)(& x));
   __clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index 9f336692a29ff1b5a71906f01a81e8137fda68b5..48ad882af35395630ea4e752ac3fbf7fdbbb5648 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -119,14 +119,16 @@ void f(void)
 
 void g(int *C, int *D)
 {
-  __store_block((void *)(& C),4U);
-  __full_init((void *)(& C));
-  __store_block((void *)(& D),4U);
-  __full_init((void *)(& D));
-  __full_init((void *)(& C));
-  C = D;
+  /*@ assert \initialized(&C); */
+  {
+    int __e_acsl_initialized;
+    __store_block((void *)(& C),4U);
+    __full_init((void *)(& C));
+    __e_acsl_initialized = __initialized((void *)(& C),sizeof(int *));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"g",
+                  (char *)"\\initialized(&C)",19);
+  }
   __delete_block((void *)(& C));
-  __delete_block((void *)(& D));
   return;
 }
 
@@ -144,51 +146,34 @@ int main(void)
   int __retres;
   int *x;
   int *y;
-  int *z;
-  int *t;
   e_acsl_global_init();
-  __store_block((void *)(& t),4U);
-  __store_block((void *)(& z),4U);
   __store_block((void *)(& y),4U);
   __store_block((void *)(& x),4U);
   __full_init((void *)(& B));
   B = (int *)__e_acsl_malloc(sizeof(int));
   __full_init((void *)(& y));
   y = (int *)__e_acsl_malloc(sizeof(int));
-  __full_init((void *)(& t));
-  t = (int *)__e_acsl_malloc(sizeof(int));
   __full_init((void *)(& x));
   x = y;
   f();
-  __full_init((void *)(& z));
-  __full_init((void *)(& t));
-  g(z,t);
   /*@ assert \initialized(&A); */
   {
     int __e_acsl_initialized;
     __e_acsl_initialized = __initialized((void *)(& A),sizeof(int *));
     e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&A)",30);
+                  (char *)"\\initialized(&A)",28);
   }
   /*@ assert \initialized(&x); */
   {
     int __e_acsl_initialized_2;
     __e_acsl_initialized_2 = __initialized((void *)(& x),sizeof(int *));
     e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&x)",31);
-  }
-  /*@ assert \initialized(&z); */
-  {
-    int __e_acsl_initialized_3;
-    __e_acsl_initialized_3 = __initialized((void *)(& z),sizeof(int *));
-    e_acsl_assert(__e_acsl_initialized_3,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&z)",32);
+                  (char *)"\\initialized(&x)",29);
   }
+  g(x,y);
   __retres = 0;
   __delete_block((void *)(& B));
   __delete_block((void *)(& A));
-  __delete_block((void *)(& t));
-  __delete_block((void *)(& z));
   __delete_block((void *)(& y));
   __delete_block((void *)(& x));
   __clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 5e20a64ef64b7eb688c6cd2f0ad837a9f7b14d55..22bf1abe67be4d1a4082f8de659c343390267f61 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -29,9 +29,17 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __malloc, behavior allocation: p
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/ptr_init.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&z);
-tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluation of
-        argument z
+tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
+[value] using specification for function __initialized
+share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
+tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function __e_acsl_malloc:
@@ -41,5 +49,11 @@ tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluatio
 [value] Values at end of function e_acsl_global_init:
 [value] Values at end of function f:
           A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+[value] Values at end of function g:
 [value] Values at end of function main:
-          NON TERMINATING FUNCTION
+          __fc_heap_status ∈ [--..--]
+          A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 5e20a64ef64b7eb688c6cd2f0ad837a9f7b14d55..22bf1abe67be4d1a4082f8de659c343390267f61 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -29,9 +29,17 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __malloc, behavior allocation: p
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/ptr_init.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&z);
-tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluation of
-        argument z
+tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
+[value] using specification for function __initialized
+share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+[value] using specification for function e_acsl_assert
+share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
+tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
+[value] using specification for function __clean
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
 [value] Values at end of function __e_acsl_malloc:
@@ -41,5 +49,11 @@ tests/e-acsl-runtime/ptr_init.c:29:[value] completely invalid value in evaluatio
 [value] Values at end of function e_acsl_global_init:
 [value] Values at end of function f:
           A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+[value] Values at end of function g:
 [value] Values at end of function main:
-          NON TERMINATING FUNCTION
+          __fc_heap_status ∈ [--..--]
+          A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
+          __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
index cc1d4258b194816e25d9fbebe367dfd856da1c0a..90576a4b9df26a3b88b53adb3c28b63f5b920202 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/ptr_init.c
@@ -27,6 +27,6 @@ int main(void) {
   f();
   /*@ assert \initialized(&A); */
   /*@ assert \initialized(&x); */
-  g(y, x);
+  g(x, y);
   return 0;
 }