diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
index 646d3b855887d7fdf258439c0fb0ee5483127a1f..d2039f2b5ee5f5dc7add5b7346d91dfabeb5e52a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
@@ -2,12 +2,6 @@
 #include "stdio.h"
 #include "stdlib.h"
 int LEN = 10;
-/*@ assigns \nothing;
-    frees p; */
- __attribute__((__FC_BUILTIN__)) void __e_acsl_delete_block(void *p);
-
-/* compiler builtin: 
-    __attribute__((__FC_BUILTIN__)) void *__builtin_alloca(unsigned long size);   */
 int main(int argc, char **argv)
 {
   int __retres;
@@ -67,6 +61,7 @@ int main(int argc, char **argv)
   }
   __retres = 0;
   __e_acsl_delete_block((void *)arr);
+  /* __fc_vla_free((void *)arr); */
   __e_acsl_delete_block((void *)(& arr));
   __e_acsl_memory_clean();
   return __retres;