diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
index 6e6816ad1d41e4d3eeedeb9f793d484bbab0921f..f95d39c1fa1c5993f16ac042f91739d2b6bfb696 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
@@ -393,7 +393,7 @@ void __e_acsl_memory_clean() {
 }
 
 /* adds argc / argv to the memory model */
-void __init_argv(int argc, char **argv) {
+static void __init_argv(int argc, char **argv) {
   int i;
 
   __store_block(argv, (argc+1)*sizeof(char*));
@@ -411,6 +411,8 @@ void __init_argv(int argc, char **argv) {
  *  ptr_size the size of the pointer computed during instrumentation. */
 void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
   arch_assert(ptr_size);
+  if (argc_ref)
+    __init_argv(*argc_ref, *argv_ref);
 }
 
 /**********************/
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index caf3d55ee513107cf33ac13f90ab4e4358829028..8fec227fc0b519277594caadf8878f8269e7fa01 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -135,11 +135,6 @@ int __offset(void * ptr)
 int __initialized(void * ptr, size_t size)
   __attribute__((FC_BUILTIN));
 
-/* put argv in the memory model */
-/*@ assigns \nothing; */
-void __init_argv(int argc, char **argv)
-	__attribute__((FC_BUILTIN));
-
 /* print the content of the abstract structure */
 void __e_acsl_memory_debug(void)
   __attribute__((FC_BUILTIN));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index 7a93e7c739707a43b21011b1c2e889ccc341f172..60e2c7f959d2d7ca4f2434c920e560de5c6f9a5b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -4,7 +4,6 @@ int main(int argc, char **argv)
   int __retres;
   int i;
   __e_acsl_memory_init(& argc,& argv,8UL);
-  __init_argv(argc,argv);
   /*@ assert \valid(&argc); */
   {
     int __e_acsl_valid;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 6b22631ba93486086aa1d4f1f66220fd84c0bba5..08d57de4d82618dfde8a2890b2f2e9bb0b6439a9 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -284,12 +284,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
           match main.sformals with
           | vi1 :: vi2 :: _
             when vi1.vtype = Cil.intType && vi2.vtype = charPtrPtrType ->
-              (* Add a call to __init_args if need argv for analysis *)
-              if Mmodel_analysis.must_model_vi vi2 then begin
-                let arg = [ Cil.evar vi1 ; Cil.evar vi2 ] in
-                let arginit = Misc.mk_call loc "__init_argv" arg in
-                main.sbody.bstmts <- arginit :: main.sbody.bstmts;
-              end;
               (* Grab addresses of arguments for a call to the main
               initialization function, i.e., [__e_acsl_memory_init] *)
               List.map Cil.mkAddrOfVi main.sformals;