diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 93dcf2ceedaa0c24035ebdd9d8d7f2928a6078c1..e2a4a854fcf6e36957015ac1e33701788ce846c3 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -311,7 +311,8 @@ do
     ;;
     --rte|-a)
       shift
-      OPTION_RTE="-rte -rte-mem -rte-no-float-to-int -no-warn-signed-overflow -no-warn-unsigned-overflow"
+      OPTION_RTE="-rte -rte-mem -rte-no-float-to-int
+        -no-warn-signed-overflow -no-warn-unsigned-overflow -then"
     ;;
     # A memory model  (or models) to link against
     -m|--memory-model)
@@ -479,11 +480,10 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
     $OPTION_FRAMA_STDLIB \
     $OPTION_FULL_MMODEL \
     $OPTION_GMP \
-    $OPTION_RTE \
     "$@" \
-    $OPTION_EACSL \
-    -print \
-    -ocode "$OPTION_OUTPUT_CODE");
+    $OPTION_RTE \
+    $OPTION_EACSL -then-last \
+    -print -ocode "$OPTION_OUTPUT_CODE");
     error "aborted by Frama-C" $?;
   # Print translated code
   if [ -n "$OPTION_PRINT" ]; then