diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 135692ddfbd8cf6cdd8d6b019bb79a554d56c4f6..5a820826ce88158bfa6b2d9b335ec700d15ed429 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -295,7 +295,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
   method !vglob_aux = function
   | GVarDecl(vi, _) | GVar(vi, _, _)
   | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
-      when Misc.is_library_loc vi.vdecl ->
+      when Misc.is_library_loc vi.vdecl || Builtins.mem vi.vname ->
     if generate then
       Cil.JustCopyPost
         (fun l ->