diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 3038810fbf9bd7f54a963b46de85a3d8c94c5129..aeb097a74dfa3380d233083835d2ca765011e62e 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -754,7 +754,9 @@ CPPFLAGS="$OPTION_CPPFLAGS"
 LDFLAGS="$OPTION_LDFLAGS"
 
 # Extra Frama-C Flags E-ACSL needs
-FRAMAC_FLAGS="$FRAMAC_FLAGS -variadic-no-translation"
+FRAMAC_FLAGS="$FRAMAC_FLAGS \
+  -remove-unused-specified-functions \
+  -variadic-no-translation"
 
 # C, CPP and LD flags for compilation of E-ACSL-generated sources
 EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT"
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 5324a4ffd3b79ee9888500d626e0543072266d62..2c2c73e7cb77419e954c8064be194206ba600c49 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -482,10 +482,6 @@ class prepare_visitor = object (self)
              [ new_decl; g ]
            | _ -> assert false)
 
-    | GVarDecl(vi, _loc) | GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc)
-      when Misc.is_fc_or_compiler_builtin vi ->
-      Cil.DoChildren
-
     | _ ->
       Cil.DoChildren
 
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 71e4991ff8be862c7bebaf66d299e9823a70e3de..2a6e96737732a5e5a0783c909d8b88d9d34cabaa 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -34,8 +34,7 @@ let create_rtl_ast prj =
   Project.on
     prj
     (fun () ->
-       (* compute the RTL AST in the same settings as the user source code.
-          Modifying these settings purposely kills the current AST (if any) *)
+       (* compute the RTL AST in the standard E-ACSL setting *)
        if Plugin.is_present "variadic" then
          Dynamic.Parameter.Bool.off "-variadic-translation" ();
        Kernel.Keep_unused_specified_functions.off ();
diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config_ci.in
index 0a68607fc713abce8bf5ac09479dd477ff07e1dd..2530bfd855acf218d3e9576d2cbdbfc32752be2a 100644
--- a/src/plugins/e-acsl/tests/test_config_ci.in
+++ b/src/plugins/e-acsl/tests/test_config_ci.in
@@ -1,7 +1,7 @@
 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: MACHDEP -machdep gcc_x86_64
 MACRO: EACSL_PREPARE -e-acsl-prepare -e-acsl-share ./share/e-acsl
-MACRO: GLOBAL @MACHDEP@ -variadic-no-translation -verbose 0
+MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -variadic-no-translation -verbose 0
 MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
 MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
 MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs