diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 2dfec7bee2c13d19d7cfee85a4701cd338264330..56ea8d22c637c6f2e9c7155b4508093b881cac2c 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -516,16 +516,33 @@ static void memory_clean() {
   bt_clean();
 }
 
-/* add `argv` to the memory model */
-static void init_argv(int argc, char **argv) {
-  int i;
+extern char **environ;
 
-  store_block(argv, (argc+1)*sizeof(char*));
-  full_init(argv);
+/* add `argv` to the memory model */
+static void argv_alloca(int *argc_ref,  char *** argv_ref) {
+  /* Track a top-level containers */
+  store_block((void*)argc_ref, sizeof(int));
+  store_block((void*)argv_ref, sizeof(char**));
+  int argc = *argc_ref;
+  char** argv = *argv_ref;
+  /* Track argv */
+
+  size_t argvlen = (argc + 1)*sizeof(char*);
+  store_block(argv, argvlen);
+  initialize(argv, (argc + 1)*sizeof(char*));
+
+  while (*argv) {
+    size_t arglen = strlen(*argv) + 1;
+    store_block(*argv, arglen);
+    initialize(*argv, arglen);
+    argv++;
+  }
 
-  for (i = 0; i < argc; i++) {
-    store_block(argv[i], strlen(argv[i])+1);
-    full_init(argv[i]);
+  while (*environ) {
+    size_t envlen = strlen(*environ) + 1;
+    store_block(*environ, envlen);
+    initialize(*environ, envlen);
+    environ++;
   }
 }
 
@@ -535,7 +552,7 @@ static void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
   initialize_report_file(argc_ref, argv_ref);
   /* Tracking program arguments */
   if (argc_ref)
-    init_argv(*argc_ref, *argv_ref);
+    argv_alloca(argc_ref, argv_ref);
   /* Tracking safe locations */
   collect_safe_locations();
   int i;
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index a4002694bf5063d8b930f61ad12038ba74afe7d3..9be817a176adb7a298e680bd34b5eda223b13f7a 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -128,6 +128,38 @@ static size_t get_heap_allocation_size(void) {
 }
 /* }}} */
 
+/* Track program arguments (ARGC/ARGV) {{{ */
+extern char ** environ;
+
+static void argv_alloca(int *argc_ref,  char *** argv_ref) {
+  /* Track a top-level containers */
+  shadow_alloca((void*)argc_ref, sizeof(int));
+  shadow_alloca((void*)argv_ref, sizeof(char**));
+  int argc = *argc_ref;
+  char** argv = *argv_ref;
+  /* Track argv */
+  size_t argvlen = (argc + 1)*sizeof(char*);
+  shadow_alloca(argv, argvlen);
+  initialize_static_region((uintptr_t)argv, (argc + 1)*sizeof(char*));
+
+  /* Track argument strings */
+  while (*argv) {
+    size_t arglen = strlen(*argv) + 1;
+    shadow_alloca(*argv, arglen);
+    initialize_static_region((uintptr_t)*argv, arglen);
+    argv++;
+  }
+
+  while (*environ) {
+    size_t envlen = strlen(*environ) + 1;
+    shadow_alloca(*environ, envlen);
+    initialize_static_region((uintptr_t)*environ, envlen);
+    environ++;
+  }
+}
+/* }}} */
+
+/* Program initialization {{{ */
 static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
   describe_run();
   /** Verify that the given size of a pointer matches the one in the present
@@ -144,7 +176,7 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
   DVALIDATE_SHADOW_LAYOUT;
   /* Track program arguments. */
   if (argc_ref && argv_ref)
-    argv_alloca(*argc_ref, *argv_ref);
+    argv_alloca(argc_ref, argv_ref);
   /* Tracking safe locations */
   collect_safe_locations();
   int i;
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index 2cce518310298d074f5a4fe8a43fc243a842ac68..45fd1e1ab79accbe17ee651efeb9a8fe883a3d1f 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -771,21 +771,6 @@ static void mark_readonly_region (uintptr_t addr, long size) {
 }
 /* }}} */
 
-/* Track program arguments (ARGC/ARGV) {{{ */
-static void argv_alloca(int argc,  char ** argv) {
-  /* Track a top-level container (i.e., `*argv`) */
-  shadow_alloca(argv, (argc + 1)*sizeof(char*));
-  initialize_static_region((uintptr_t)argv, (argc + 1)*sizeof(char*));
-  /* Track argument strings */
-  while (*argv) {
-    size_t arglen = strlen(*argv) + 1;
-    shadow_alloca(*argv, arglen);
-    initialize_static_region((uintptr_t)*argv, arglen);
-    argv++;
-  }
-}
-/* }}} */
-
 /* Heap allocation {{{ (malloc/calloc) */
 
 /*! \brief Amount of heap memory allocated by the program.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
index 7787974a78645a3f0769e05b917875be64023ed0..4e7868fd36b6ec24a6eae265c88ea1cbe0fb1fd8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
@@ -4,7 +4,6 @@ int main(int argc, char const **argv)
 {
   int __retres;
   __e_acsl_memory_init(& argc,(char ***)(& argv),(size_t)8);
-  __e_acsl_store_block((void *)(& argc),(size_t)4);
   goto L;
   {
     int *p;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index f0a7e6b8479128adb4c0d2fe5d0290b0cf167f69..6377f308afc58b56690c2450bf6c33fc49413961 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -9,8 +9,6 @@ int main(int argc, char **argv)
   /*@ assert \valid(&argc); */
   {
     int __gen_e_acsl_valid;
-    __e_acsl_store_block((void *)(& argv),(size_t)8);
-    __e_acsl_store_block((void *)(& argc),(size_t)4);
     __gen_e_acsl_valid = __e_acsl_valid((void *)(& argc),sizeof(int),
                                         (void *)(& argc),(void *)(& argc));
     __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 767ea2bc422be18d17db6975f08b7e7e9e0e7501..2bfb8b9f0afa8aa9b1f2d005adb70adcd9256831 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -524,8 +524,10 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       if self#is_first_stmt kf stmt then
         (* JS: should be done in the new project? *)
         let env =
-          if generate then Memory.store env kf (Kernel_function.get_formals kf)
-          else env
+          if generate && not is_main then
+            Memory.store env kf (Kernel_function.get_formals kf)
+          else
+            env
         in
         (* translate the precondition of the function *)
         if Dup_functions.is_generated (Extlib.the self#current_kf) then