diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 9c0be44c094927cd44edf3d1666ede2592be004e..02b4b7faa95a33954802c207666dc309f3d2b669 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -434,7 +434,9 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
        the final block does not contain any local, so may be transient. *)
     if split then
       match stmt.skind with
-      | Instr (Skip _) -> b
+      (* [TODO ARCHI] would result in nicer generated pieces of code, but
+       * killing statements has huge consequences on Frama-C invariants... *)
+      (*      | Instr (Skip _) -> b *)
       | _ ->
         let sblock = Cil.mkStmt ~valid_sid:true (Block b) in
         Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 43ea6d2192fe0e4bc32ea29db6a396bcb6de1d6e..10ff14fd0dde9a91e96867ed05aad284324fba4c 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -348,6 +348,7 @@ let add_new_block_in_stmt env kf stmt =
     "@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt;
   new_stmt, env
 
+(* [TODO ARCHI] not sure returning the stmt_kind is useful *)
 (* visit the substmts and build the new skind *)
 let rec inject_in_substmt env kf stmt = match stmt.skind with
   | Instr instr ->
@@ -748,23 +749,28 @@ let inject_in_file file =
   file.globals <- Logic_functions.add_generated_functions file.globals;
   inject_mmodel_initializer main
 
-let reset_all () =
+let reset_all ast =
+  Options.Run.off ();
   Misc.reset ();
   Logic_functions.reset ();
   Literal_strings.reset ();
   Global_observer.reset ();
-  Keep_status.before_translation ()
+  Typing.clear ();
+  Cfg.clearFileCFG ~clear_id:false ast;
+  Cfg.computeFileCFG ast;
+  Kernel_function.clear_sid_info ();
+  Ast.mark_as_grown ()
 
 let inject () =
   Options.feedback ~level:2
     "injecting annotations as code in project %a"
     Project.pretty (Project.current ());
-  reset_all ();
+  Keep_status.before_translation ();
   Misc.reorder_ast ();
   let ast = Ast.get () in
   inject_in_file ast;
-  (* [TODO ARCHI] not consistent with the [reset_all] strategy: *)
-  Typing.clear ()
+  Loops.apply_after_transformation ();
+  reset_all ast;
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index eb4b4dd749380fbc85e19a4cad20d61bc09a2a7b..d8b4ff6664ed12b9e98ed1341e8a7dd6cb8785d8 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -45,8 +45,7 @@ let term_to_exp_ref
 
 module Loop_invariants_actions = Hook.Make(struct end)
 
-let apply_after_transformation prj =
-  Project.on prj Loop_invariants_actions.apply ()
+let apply_after_transformation = Loop_invariants_actions.apply
 
 let mv_invariants kf ~old stmt =
   Options.feedback ~current:true ~level:3
diff --git a/src/plugins/e-acsl/src/code_generator/loops.mli b/src/plugins/e-acsl/src/code_generator/loops.mli
index a37b5beaee75b7eb470edb30c99f3504d1857425..a93afb4cb6b93e55b595317087f59edbb9ca4b3e 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.mli
+++ b/src/plugins/e-acsl/src/code_generator/loops.mli
@@ -28,7 +28,7 @@ open Cil_types
 (************************* Loop invariants ********************************)
 (**************************************************************************)
 
-val apply_after_transformation: Project.t -> unit
+val apply_after_transformation: unit -> unit
 
 val mv_invariants: kernel_function -> old:stmt -> stmt -> unit
 (** Transfer the loop invariants from the [old] loop to the new one.
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 4b0ccaabdf1c6e5537240e633ed71313e03aa1de..04623b1a012cff399d47a9b5d13bf6841c1ff98f 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -151,8 +151,6 @@ let generate_code =
                         Gmp_types.init ();
                         Mmodel_analysis.reset ();
                         Injector.inject ();
-                        (* [TODO ARCHI] remove the project as arguments *)
-                        Loops.apply_after_transformation copied_prj;
                         (* remove the RTE's results computed from E-ACSL:
                            they are partial and associated with the wrong
                            kernel function (the one of the old project). *)