diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index c9c6d57ad0c73ec729c54283b2ee229358132cca..57741158f654d5709468fec593b4a3317fc57aa9 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -191,16 +191,15 @@ let dup_fundec loc spec bhv kf vi new_vi =
     sbody = body;
     smaxstmtid = None;
     sallstmts = [];
-    sspec = new_spec }, 
-  return
+    sspec = new_spec }
 
 let dup_global loc old_prj spec bhv kf vi new_vi = 
   let name = vi.vname in
   Options.feedback ~dkey ~level:2 "entering in function %s" name;
-  let fundec, return = dup_fundec loc spec bhv kf vi new_vi  in
+  let fundec = dup_fundec loc spec bhv kf vi new_vi  in
   let fct = Definition(fundec, loc) in
   let new_spec = fundec.sspec in
-  let new_kf = { fundec = fct; return_stmt = Some return; spec = new_spec } in
+  let new_kf = { fundec = fct; spec = new_spec } in
   Kernel_function.Hashtbl.add fct_tbl new_kf ();
   Globals.Functions.register new_kf;
   Globals.Functions.replace_by_definition new_spec fundec loc;
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index fa9e17d473c0cc2d400bafa0fe68bde833f6ca73..03b1c827851f4a6b18a79f46af556bf71e25818f 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -206,7 +206,7 @@ class e_acsl_visitor prj generate = object (self)
               (* Create and register [__e_acsl_globals_init] as kernel
                  function *)
               let kf =
-                { fundec = fct; return_stmt = Some return; spec = spec }
+                { fundec = fct; spec = spec }
               in
               Globals.Functions.register kf;
               Globals.Functions.replace_by_definition