diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
index 9ae1f7c21ddc07f63bc7df4fb9bc58cd321fc08b..6677db53488571ae0cb179d7c6504944131f9cd8 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = -3;
   int y = 2;
   long z = 2L;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
index b5a38e3d9d550321295f8dbc1d106711339907bd..334e1f1891acd45ad6414ea94e962a4e8325adf2 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
@@ -6,7 +6,6 @@ int T2[4];
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     int i = 0;
     while (i < 3) {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
index 1d262fa573a8968eb3baee7c27bb2fac552e0bb5..c5a5d0cce531b902d925bd9b435b23ff6b64d963 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   long x = (long)0;
   int y = 0;
   __e_acsl_assert((int)x == y,"Assertion","main","(int)x == y",
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
index 80676d549eb3bb932c301f5540ea2683166304be..08496d44c2396e09142e025ace2d5fe9aec84610 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   __e_acsl_assert(x < y,"Assertion","main","x < y",
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index c5a633e03505673ed4d11a1effefc365b23443d7..f8431536df11c96f3b9ef987ed96d87d51eba02a 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -85,7 +85,6 @@ int main(void)
 {
   int __retres;
   mystruct m;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 1;
   int y = 2;
   {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index b6a6fd8abf5cea178fca6f88b540f92a59ac141f..6b5f403f5a2f68d0bc58eed95b7ebd913c9c41cc 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -38,7 +38,6 @@ unsigned long __gen_e_acsl_f4_2(long n);
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     __e_acsl_mpz_t __gen_e_acsl_f1_6;
     __e_acsl_mpz_t __gen_e_acsl__3;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
index f9c0176310cf6eec2bfd33baa69cc60ff361303a..15a95e1655951a6ae8a649d80881877aff06af4b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
@@ -5,7 +5,6 @@ int main(void)
 {
   int __retres;
   int x;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_assert(1,"Assertion","main","0 == 0",
                   "tests/arith/integer_constant.i",6);
   /*@ assert 0 ≡ 0; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 9278b61ce9f86648b663fe7cb7ade212b1857410..7ee8de540851b4cfc13f744c22e4e0271e5e0561 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -26,7 +26,6 @@ unsigned long long my_pow(unsigned int x, unsigned int n)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   unsigned long long x = my_pow((unsigned int)2,(unsigned int)63);
   {
     __e_acsl_mpz_t __gen_e_acsl_;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
index 9426f228f9aef4d7b5589cb07889c6084df51c65..4ba24ca0879edf6173547ef7665fe0dfd3b135de 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   __e_acsl_assert(x == 0,"Assertion","main","x == 0","tests/arith/not.i",6);
   /*@ assert x ≡ 0; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index 8d7127bbb6383e83b6e645ba2300b1e5b3f95ef5..bd22a341b9b2fb5c25072ebb4b661bfbbac0f19f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -19,7 +19,6 @@ double avg(double a, double b)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     __e_acsl_mpq_t __gen_e_acsl_;
     __e_acsl_mpq_t __gen_e_acsl__2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
index f9def933ef75326a30452f1c36516c48a5288ccb..66f0d9080e4c01efc18f40664b68ffd58b5a5119 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
@@ -25,7 +25,6 @@ int fact(int n)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = __gen_e_acsl_fact(5);
   __e_acsl_assert(x == 120,"Assertion","main","x == 120",
                   "tests/bts/bts1395.i",14);
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
index 869af38e287486855fd54b901886ef56a91caf92..6dddd2a40459ae418afc2b9a752964fe125984dc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
@@ -53,6 +53,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& global_i_ptr));
+  __e_acsl_delete_block((void *)(& global_i));
+}
+
 int main(void)
 {
   int __retres;
@@ -60,8 +66,7 @@ int main(void)
   __e_acsl_globals_init();
   __gen_e_acsl_loop();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& global_i_ptr));
-  __e_acsl_delete_block((void *)(& global_i));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
index 20ab35b8cb019792f609cad02946e874a71bd89e..0c35a1254beda7c48905f510b8cd0b0ae4af49f9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
@@ -88,6 +88,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& S));
+}
+
 int main(void)
 {
   int __retres;
@@ -144,7 +149,7 @@ int main(void)
   }
   f();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& S));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
index 809a47170c6359d63984dc7c997463a7d5fc9a5d..41b668706f86030c287a11992ef37b9fd3328d1c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
@@ -31,6 +31,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(_G));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -55,7 +60,7 @@ int main(int argc, char **argv)
   }
   /*@ assert \valid_read(_G[0].str); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(_G));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
index 5cd324316570b0133733102547a312cdef4c3b3f..02dcc62330216104b4a830f0aac14181c43ae900 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
@@ -21,6 +21,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& n));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -29,7 +34,7 @@ int main(int argc, char **argv)
   argc = __gen_e_acsl_atoi((char const *)n);
   a = argc;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& n));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
index 64ef82e9bf903467868e6fc87904a2957811d739..e3887d10a705e41beb1f739df200ac7a574232ae 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
@@ -5,7 +5,6 @@ long A = (long)0;
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     __e_acsl_mpz_t __gen_e_acsl_A;
     __e_acsl_mpz_t __gen_e_acsl_;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
index 29d1004ec5b7ebcd3a8136c1bb4a313979aa7184..55454d5d36b67f3bfc10e27db0a1244dc5b64ba7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
@@ -24,6 +24,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& t));
+}
+
 int main(int argc, char **argv)
 {
   int tmp;
@@ -35,7 +40,7 @@ int main(int argc, char **argv)
   t.j = (_Bool)1;
   /*@ assert \initialized(&t.j); */ ;
   tmp = test(& t);
-  __e_acsl_delete_block((void *)(& t));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return tmp;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
index 8e24a58e6223bf92569de8db4eb0e67f6ee23db5..3dbfd57c93af5c2095db14eb114db36d0ea21f89 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
@@ -14,6 +14,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(t));
+}
+
 int main(void)
 {
   int __retres;
@@ -39,8 +44,8 @@ int main(void)
   }
   /*@ assert \valid(&t[0 .. 9]); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(t));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
index cbc6c2e0d193f650e3ad3e14d969d8ba58d1518a..44cfac328f8ff8637b0acf5384c359fa86b3ea1b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     int __gen_e_acsl_forall;
     int __gen_e_acsl_c;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
index ffb55240c93494ac3528ad961f911ea9c45767fc..7c2dc5ed4699cd1b21b3a8a1a2b331de709d4da0 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   if (x) {
     __e_acsl_assert(0,"Assertion","main","\\false",
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
index dcfe6a61c3fd5c6f03344258a6165871a104c588..9e7f63becc8b260a7c45ea04dcb5d33350f77fdd 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
@@ -129,7 +129,6 @@ void n(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __gen_e_acsl_f();
   __gen_e_acsl_g();
   __gen_e_acsl_h();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
index e942d64b232a327b604995b2a34c219ae3ed5553..ab2bc7b703821eac9e38b82846f04b971497d3c5 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& P));
+  __e_acsl_delete_block((void *)(& G));
+}
+
 int main(void)
 {
   int __retres;
@@ -67,9 +73,8 @@ int main(void)
     G ++;
   }
   __retres = 0;
-  __e_acsl_delete_block((void *)(& P));
-  __e_acsl_delete_block((void *)(& G));
   __e_acsl_delete_block((void *)(& q));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
index 226d6482951d71ee138e647e9fa4a65417894720..803e14a2914f164781f4cd2324420ffc2567e370 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   {
     int i = 0;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
index c364fb15de4e27537de95c6d4e448d0b83823e5b..06a5de92573cd1f63bb730d2872ce69f3432a319 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
@@ -40,7 +40,6 @@ int __gen_e_acsl_main(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __retres = __gen_e_acsl_main();
   __e_acsl_assert(X == 3,"Postcondition","main","X == 3",
                   "tests/constructs/labeled_stmt.i",7);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
index 72434006bf47588df548c0678e4b112bc3dc58b7..b9ba06467be864939e8f22b5f52bfe826b1b814e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   {
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
index 2626d70b85c3bea55d62ce250c25c032162e59f1..879d1ee52a8ea1608999651843b866fc15f8f381 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
@@ -183,7 +183,6 @@ void unnatural_loop(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   simple_loop();
   nested_loops();
   unnatural_loop();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
index 9411fb1ecd898231338a95b44f172fd3e1cce1e2..252046ac3c885a76d1db75b9e766725b2a12340b 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 1;
   __e_acsl_assert(x < y,"Assertion","main","x < y",
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
index 88919141b53aa7d6efcdc5340f0a56d232ca002d..6b0f6fcf6b200810222c7a03b36bd41a2d2b6526 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
@@ -35,7 +35,6 @@ int h(void)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __gen_e_acsl_f(1);
   __gen_e_acsl_g(Y);
   __gen_e_acsl_h();
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
index 0fc68d324f2eb5da8ce6809cee84eff4ef73e042..b9942c443b734d7b8125e9eb9632e5a9e0a1cd03 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   int y = 2;
   /*@ ensures x ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
index f8a614b4c4852a3de940e41309b9bd66939114b8..243f60598a1d7058fdac1047fc7513c4dea1bc85 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   x ++;
   __e_acsl_assert(1,"Assertion","main","\\true","tests/constructs/true.i",8);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
index 7b74563fa1e006d1c03eab9cb71b0c58329ff459..92e02166357ca38676b0a54bdfe18e6b4a1015b6 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
@@ -5,7 +5,6 @@ typedef unsigned char uint8;
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   uint8 x = (unsigned char)0;
   __e_acsl_assert((int)x == 0,"Assertion","main","x == 0",
                   "tests/constructs/typedef.i",9);
diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
index 09509e5c90ae60ba35b72a502589d90688aef2d7..6657c1ae8ee2ab44422f5fe7bf30ed3f45503d99 100644
--- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
@@ -102,7 +102,6 @@ int main(void)
 {
   int __retres;
   int found;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   {
     int i = 0;
     while (i < 10) {
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
index a96c903d115bcde7976d3b96ab1b10bcdd5c5d73..ca3a611c9bd240c6dba0d59cbea332b76cbe4f44 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
@@ -57,6 +57,20 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& f));
+  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
+  __e_acsl_delete_block((void *)(__fc_tmpnam));
+  __e_acsl_delete_block((void *)(& __fc_p_fopen));
+  __e_acsl_delete_block((void *)(__fc_fopen));
+  __e_acsl_delete_block((void *)(& stdin));
+  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
+  __e_acsl_delete_block((void *)(random48_counter));
+  __e_acsl_delete_block((void *)(& __fc_random48_init));
+  __e_acsl_delete_block((void *)(& __fc_rand_max));
+}
+
 int main(void)
 {
   int __retres;
@@ -72,18 +86,9 @@ int main(void)
   /*@ assert &x ≡ &x; */ ;
   __e_acsl_full_init((void *)(& __retres));
   __retres = 0;
-  __e_acsl_delete_block((void *)(& f));
-  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
-  __e_acsl_delete_block((void *)(__fc_tmpnam));
-  __e_acsl_delete_block((void *)(& __fc_p_fopen));
-  __e_acsl_delete_block((void *)(__fc_fopen));
-  __e_acsl_delete_block((void *)(& stdin));
-  __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
-  __e_acsl_delete_block((void *)(random48_counter));
-  __e_acsl_delete_block((void *)(& __fc_random48_init));
-  __e_acsl_delete_block((void *)(& __fc_rand_max));
   __e_acsl_delete_block((void *)(& x));
   __e_acsl_delete_block((void *)(& __retres));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index 721e12502219c7738e2547f6a0bd1ac1f5a6722b..dc901aa064e92b92e00e8c4b63a5fb05f813fca9 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = -3;
   int y = 2;
   long z = 2L;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index f47d15dc1de8409ff9909b8e03349666e21302b8..25a8fe984219cdd86055a1fc7173d91303cc1530 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -83,7 +83,6 @@ int main(void)
 {
   int __retres;
   mystruct m;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 1;
   int y = 2;
   {
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
index 6f888df6d065d78c22c954269449c6aa082a292c..9f45f3d678f16d88ce64d3a27351bafe295429bc 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& PA));
+  __e_acsl_delete_block((void *)(A));
+}
+
 int main(void)
 {
   int __retres;
@@ -311,8 +317,6 @@ int main(void)
   }
   /*@ assert \base_addr(q) ≡ \base_addr(qd); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& PA));
-  __e_acsl_delete_block((void *)(A));
   __e_acsl_delete_block((void *)(& qd));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& pd));
@@ -322,6 +326,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& l));
   __e_acsl_delete_block((void *)(& pa));
   __e_acsl_delete_block((void *)(a));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
index 4f0f4366d63a92caa4c16a1376aef65e6e0c0fdd..4cbe891d458c6fac7738d2ce38d0b5fc3b5e6a98 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
@@ -22,6 +22,13 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& ZERO));
+  __e_acsl_delete_block((void *)(& PA));
+  __e_acsl_delete_block((void *)(A));
+}
+
 int main(void)
 {
   int __retres;
@@ -238,9 +245,6 @@ int main(void)
   }
   /*@ assert \block_length(q) ≡ size; */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& ZERO));
-  __e_acsl_delete_block((void *)(& PA));
-  __e_acsl_delete_block((void *)(A));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
   __e_acsl_delete_block((void *)(& pi));
@@ -249,6 +253,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& pa));
   __e_acsl_delete_block((void *)(a));
   __e_acsl_delete_block((void *)(& zero));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
index a839a6888e5457bdd352c8bbff5536f6cc609bd6..3871a01e451cfe6dde011661ac2b0b4942854639 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
@@ -15,6 +15,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& B));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -151,11 +156,11 @@ int main(int argc, char **argv)
   }
   /*@ assert ¬\valid(pmax - diff); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& B));
   __e_acsl_delete_block((void *)(& pmax));
   __e_acsl_delete_block((void *)(& pmin));
   __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
index e10793f41018677657e111efbaf3f8b81307a83e..a5c535378151910cf595a16301c5ac72aa331ff9 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
@@ -65,6 +65,17 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(_G));
+  __e_acsl_delete_block((void *)(& _E));
+  __e_acsl_delete_block((void *)(_D));
+  __e_acsl_delete_block((void *)(& _C));
+  __e_acsl_delete_block((void *)(& _B));
+  __e_acsl_delete_block((void *)(_A));
+  __e_acsl_delete_block((void *)(& _F));
+}
+
 int main(int argc, char **argv)
 {
   int __retres;
@@ -176,13 +187,7 @@ int main(int argc, char **argv)
                   "tests/memory/compound_initializers.c",43);
   /*@ assert _G[0].num ≡ 99; */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(_G));
-  __e_acsl_delete_block((void *)(& _E));
-  __e_acsl_delete_block((void *)(_D));
-  __e_acsl_delete_block((void *)(& _C));
-  __e_acsl_delete_block((void *)(& _B));
-  __e_acsl_delete_block((void *)(_A));
-  __e_acsl_delete_block((void *)(& _F));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
index f8a0d9b78f7f2b704c58c6b33afcdaaebc45ad89..cc458e4e367b7f4f52387e3d42d727f7ff9f4df6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& errno));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -38,8 +43,8 @@ int main(int argc, char const **argv)
   }
   /*@ assert \valid(p); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& errno));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
index 57d0968b67750997726a2d69abdb2203f2206f79..6504639acc77d78fee02adba6c18807b8d3d0c27 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(array));
+}
+
 int main(void)
 {
   int __retres;
@@ -75,8 +80,8 @@ int main(void)
   }
   /*@ assert ¬\freeable(&array[5]); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(array));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
index 21e0d8d49e93362922685b0c1538a1026d24bedf..dcd56fb12c71d3ca2e9cc8fa528992df29cc0cd0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
@@ -9,7 +9,6 @@ void function(int a, int b, int c, int d)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int w = 0;
   int x = 1;
   int y = 2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
index ac4c3251956faf3ce1a4ee25379caa79d892b195..d5c1542ac4f7e43c2a39612fd1f6f8b8205fc76c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
@@ -13,6 +13,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& a));
+}
+
 int main(void)
 {
   int __retres;
@@ -34,8 +39,8 @@ int main(void)
   }
   /*@ assert \initialized(b); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& a));
   __e_acsl_delete_block((void *)(& b));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
index 97f4520a88aef0c989249eab9a2abc1c9c02cb2f..e3a9201614e27d12a529b3bf3b659e3654f02192 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& b));
+  __e_acsl_delete_block((void *)(& a));
+}
+
 int main(void)
 {
   int __retres;
@@ -45,10 +51,9 @@ int main(void)
   }
   /*@ assert \initialized(p); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& b));
-  __e_acsl_delete_block((void *)(& a));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
index c426b1e926591f79e583da1089d6e600480e80dc..026e4bbef144f7d8a119f8d9d5fee687fb3f4dd6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& B));
+  __e_acsl_delete_block((void *)(& A));
+}
+
 int main(void)
 {
   int __retres;
@@ -352,8 +358,6 @@ int main(void)
   dup[0] = 1;
   dup[0] = 1;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& B));
-  __e_acsl_delete_block((void *)(& A));
   __e_acsl_delete_block((void *)(d));
   __e_acsl_delete_block((void *)(c));
   __e_acsl_delete_block((void *)(& r));
@@ -361,6 +365,7 @@ int main(void)
   __e_acsl_delete_block((void *)(& a));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
index 3dbfb76f1f0296ca96e263e5bd18e3cacd55021f..74ba7f26de69c765049127433fb50106aa2b6dfd 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
@@ -82,6 +82,15 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& l_str));
+  __e_acsl_delete_block((void *)(& s_str));
+  __e_acsl_delete_block((void *)(& S2));
+  __e_acsl_delete_block((void *)(& S));
+  __e_acsl_delete_block((void *)(& T));
+}
+
 int main(void)
 {
   int __retres;
@@ -138,12 +147,8 @@ int main(void)
   s_str ++;
   l_str ++;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& l_str));
-  __e_acsl_delete_block((void *)(& s_str));
-  __e_acsl_delete_block((void *)(& S2));
-  __e_acsl_delete_block((void *)(& S));
-  __e_acsl_delete_block((void *)(& T));
   __e_acsl_delete_block((void *)(& SS));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
index 2556be7d0248ecfe121130a372fa8be4fa7cbe03..1f7424a1ec1eae755ed5ec0b6ae0b5c396c36c94 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
@@ -22,6 +22,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& p));
+  __e_acsl_delete_block((void *)(& X));
+}
+
 int main(void)
 {
   int __retres;
@@ -29,8 +35,7 @@ int main(void)
   __e_acsl_globals_init();
   f();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& p));
-  __e_acsl_delete_block((void *)(& X));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
index ba7b47ef1efb3dcf236f93b079d608c747538631..02d31514dd514a5bfd5f727e2be47391a94815c2 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_assert((void *)0 == (void *)0,"Assertion","main",
                   "\\null == (void *)0","tests/memory/null.i",6);
   /*@ assert \null ≡ (void *)0; */ ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
index 5c92ba3302262ac4dafabd204b8630980d5cac1b..4ce316ea42cfb59cd90e1929990019505f16440e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
@@ -16,6 +16,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& PA));
+  __e_acsl_delete_block((void *)(A));
+}
+
 int main(void)
 {
   int __retres;
@@ -208,14 +214,13 @@ int main(void)
   }
   /*@ assert \offset(q) ≡ sizeof(long) * 7; */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& PA));
-  __e_acsl_delete_block((void *)(A));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
   __e_acsl_delete_block((void *)(& pi));
   __e_acsl_delete_block((void *)(& pl));
   __e_acsl_delete_block((void *)(& l));
   __e_acsl_delete_block((void *)(a));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
index 1af62be53369d574c402c31fd5c59bb7c192637c..e6f639fa93586a5740844dada0ba1163d4c1fc34 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
@@ -8,7 +8,6 @@ enum bool {
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   __e_acsl_assert(1,"Assertion","main","\'c\' == \'c\'",
                   "tests/memory/other_constants.i",10);
   /*@ assert 'c' ≡ 'c'; */ ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
index 91f376c34796a2f330bac280083e03fb8e6a9e5b..e021ea6783c863b45d6d1911bf9f1b6ba0536757 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
@@ -32,6 +32,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& B));
+  __e_acsl_delete_block((void *)(& A));
+}
+
 int main(void)
 {
   int __retres;
@@ -60,10 +66,9 @@ int main(void)
   /*@ assert \initialized(&x); */ ;
   g(x,y);
   __retres = 0;
-  __e_acsl_delete_block((void *)(& B));
-  __e_acsl_delete_block((void *)(& A));
   __e_acsl_delete_block((void *)(& y));
   __e_acsl_delete_block((void *)(& x));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
index 0439ae760d247323b99500285a5e4fa68a30ba09..7920e6b98d14aa615660abce4145ecb3cb3ea401 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
@@ -4,7 +4,6 @@
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int x = 0;
   x ++;
   __e_acsl_assert(1,"Assertion","main","sizeof(int) == sizeof(x)",
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
index f9b0f156e87318aee8dedbc78a7ba7938e883a35..49ec6cf163ec5ba0edfad147a4fa237e95bb0678 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
@@ -16,6 +16,13 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& stdout));
+  __e_acsl_delete_block((void *)(& stdin));
+  __e_acsl_delete_block((void *)(& stderr));
+}
+
 int main(void)
 {
   int __retres;
@@ -46,9 +53,7 @@ int main(void)
   }
   /*@ assert \valid(__fc_stdout); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(& stdout));
-  __e_acsl_delete_block((void *)(& stdin));
-  __e_acsl_delete_block((void *)(& stderr));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
index 70735ca3898ab082aed8f735f4d730a7589ad0fc..38b803a26a325b0b7f87db4a9117ad74d7359762 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
@@ -137,6 +137,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& Z));
+  __e_acsl_delete_block((void *)(& X));
+}
+
 int main(void)
 {
   int __retres;
@@ -521,13 +527,12 @@ int main(void)
   /*@ assert \valid(&Z); */ ;
   g();
   __retres = 0;
-  __e_acsl_delete_block((void *)(& Z));
-  __e_acsl_delete_block((void *)(& X));
   __e_acsl_delete_block((void *)(& n));
   __e_acsl_delete_block((void *)(& d));
   __e_acsl_delete_block((void *)(& c));
   __e_acsl_delete_block((void *)(& b));
   __e_acsl_delete_block((void *)(& a));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
index 0678e6d623602828c51fde50fe13cb6ec0b5c6e2..dcc566b58e8566c1d56d8ef15dbf2bd961ea6918 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
@@ -24,7 +24,6 @@ int incr(int x)
 int main(void)
 {
   int __retres;
-  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   int i = __gen_e_acsl_f(2);
   __retres = 0;
   return __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
index ca59330238b1a3b7d7df6ab8aa7a29843acc1581..f2c564d40b49843100e080bb245424a1ef3e40e1 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
@@ -58,6 +58,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(Vertices2));
+  __e_acsl_delete_block((void *)(Vertices));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -105,13 +111,12 @@ int main(int argc, char const **argv)
   __e_acsl_temporal_save_nblock_parameter((void *)(triple_vertices2[0]),0U);
   abe_matrix(triple_vertices2[0]);
   __retres = 0;
-  __e_acsl_delete_block((void *)(Vertices2));
-  __e_acsl_delete_block((void *)(Vertices));
   __e_acsl_delete_block((void *)(triple_vertices2));
   __e_acsl_delete_block((void *)(triple_vertices));
   __e_acsl_delete_block((void *)(vertices3));
   __e_acsl_delete_block((void *)(vertices2));
   __e_acsl_delete_block((void *)(vertices));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
index 4a0750a1833961e9cc5ed7bee0ea397cba57e6e2..6ce50be381f69a319c1fed912c25b458a733a14b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
@@ -18,6 +18,11 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(& foo));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -61,10 +66,10 @@ int main(int argc, char const **argv)
   /*@ assert \valid(q); */ ;
   __retres = 0;
   __e_acsl_delete_block((void *)(& argc));
-  __e_acsl_delete_block((void *)(& foo));
   __e_acsl_delete_block((void *)(& fp));
   __e_acsl_delete_block((void *)(& q));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
index d1c0cc7c58f5b37b821cdef493dea621b1a313f6..1a223bf90f4bb66628d86a49641066fc554af8cc 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
@@ -110,6 +110,16 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(descs2));
+  __e_acsl_delete_block((void *)(& l_desc2));
+  __e_acsl_delete_block((void *)(descs));
+  __e_acsl_delete_block((void *)(& l_desc));
+  __e_acsl_delete_block((void *)(extra_lbits));
+  __e_acsl_delete_block((void *)(strings));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -193,13 +203,8 @@ int main(int argc, char const **argv)
   }
   /*@ assert \valid_read(*p); */ ;
   __retres = 0;
-  __e_acsl_delete_block((void *)(descs2));
-  __e_acsl_delete_block((void *)(& l_desc2));
-  __e_acsl_delete_block((void *)(descs));
-  __e_acsl_delete_block((void *)(& l_desc));
-  __e_acsl_delete_block((void *)(extra_lbits));
-  __e_acsl_delete_block((void *)(strings));
   __e_acsl_delete_block((void *)(& p));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
index b6341802859d40a4fa7482e3bd7206f0c98f8bd3..9ccb27aa258ca9cd5f58e030f4523d3535aec27f 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
@@ -106,6 +106,12 @@ void __e_acsl_globals_init(void)
   return;
 }
 
+void __e_acsl_globals_delete(void)
+{
+  __e_acsl_delete_block((void *)(Str));
+  __e_acsl_delete_block((void *)(Strings));
+}
+
 int main(int argc, char const **argv)
 {
   int __retres;
@@ -411,8 +417,6 @@ int main(int argc, char const **argv)
   __e_acsl_temporal_save_nblock_parameter((void *)(& descs2[1].desc),0U);
   build_tree(& descs2[1].desc);
   __retres = 0;
-  __e_acsl_delete_block((void *)(Str));
-  __e_acsl_delete_block((void *)(Strings));
   __e_acsl_delete_block((void *)(descs2));
   __e_acsl_delete_block((void *)(& l_desc2));
   __e_acsl_delete_block((void *)(descs));
@@ -422,6 +426,7 @@ int main(int argc, char const **argv)
   __e_acsl_delete_block((void *)(str));
   __e_acsl_delete_block((void *)(& p));
   __e_acsl_delete_block((void *)(strings));
+  __e_acsl_globals_delete();
   __e_acsl_memory_clean();
   return __retres;
 }