diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 639f914e55fd3007af0aa9c919006c9b4782734a..c28471d3f8965330d92318edda423fb803a8dad7 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -73,5 +73,7 @@ doc/doxygen/html
 doc/doxygen/warn.log
 lib/libeacsl-jemalloc.a
 lib/libeacsl-gmp.a
-lib/libeacsl-bittree-rtl.a
-lib/libeacsl-segment-rtl.a
+lib/libeacsl-bittree-rtl-opt.a
+lib/libeacsl-segment-rtl-opt.a
+lib/libeacsl-bittree-rtl-debug.a
+lib/libeacsl-segment-rtl-debug.a
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 0adea0bae404df6da462dbd24af154ce1d6ae16c..3c2275c69bf396a2f6ea28eab266e1249f4b4929 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -183,35 +183,40 @@ EACSL_SHARE := $(EACSL_PLUGIN_DIR)/share/e-acsl
 
 EACSL_RTL_SRC = $(wildcard $(EACSL_SHARE)/*.[ch] $(EACSL_SHARE)/*/*.[ch])
 
-RTLFAGS = -std=c99 -Wall -Wno-unused -Wno-attributes -I$(EACSL_SHARE) \
+RTLFLAGS = -std=c99 -Wall -Wno-unused -Wno-attributes -I$(EACSL_SHARE) \
   -fno-omit-frame-pointer -DE_ACSL_BUILTINS
 
-ifeq (@OPTIMIZED_RTL@,no)
-RTLFAGS += -DE_ACSL_DEBUG -g3 -O0
-else
-RTLFAGS += -O2
-endif
+RTLOPT 	 = $(RTLFLAGS) -O2
+RTLDEBUG = $(RTLFLAGS) -DE_ACSL_DEBUG -g3 -O0
 
 # Build a static library
   # $1 Compile-time flags
   # $2 Library path
   # $3 Source files
 MKRTL = \
+	echo "Making $2"; \
   object=$$(basename -s .a $2).o && \
-  echo 'CC          $3' && \
+  echo ' CC $3' && \
   $(CC) $1 -c -o$$object $3 && \
-  echo 'AR          $2' && \
+  echo ' AR $2' && \
   $(AR) crus $2 $$object && \
   $(RM) -f $$object && \
   ranlib $2
 
-$(EACSL_LIBDIR)/libeacsl-%-rtl.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC)
-	$(call MKRTL, $(RTLFAGS), $@, $<)
+$(EACSL_LIBDIR)/libeacsl-%-rtl-opt.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC)
+	$(call MKRTL, $(RTLOPT),$@,$<,Optimized bittree)
+
+$(EACSL_LIBDIR)/libeacsl-%-rtl-debug.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC)
+	$(call MKRTL,$(RTLDEBUG),$@,$<,debug)
 
-EACSL_RTL = $(EACSL_LIBDIR)/libeacsl-bittree-rtl.a
+EACSL_RTL = \
+	$(EACSL_LIBDIR)/libeacsl-bittree-rtl-opt.a \
+	$(EACSL_LIBDIR)/libeacsl-bittree-rtl-debug.a
 
 ifneq ($(wildcard $(EACSL_SHARE)/segment_model),)
-  EACSL_RTL += $(EACSL_LIBDIR)/libeacsl-segment-rtl.a
+EACSL_RTL += \
+	$(EACSL_LIBDIR)/libeacsl-segment-rtl-opt.a \
+	$(EACSL_LIBDIR)/libeacsl-segment-rtl-debug.a
 endif
 
 clean::
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index 1e306468bcda5e8eba411ea499985770e01abfd4..e801b7b5bb4fec8d9e0f76df390eb79e828a3389 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -110,13 +110,6 @@ AC_ARG_ENABLE(full-gmp,
     ["Disable runtime assertions in the RTL"]),
     [FULL_GMP="yes"],[FULL_GMP="no"])
 
-# RTL
-#####
-AC_ARG_ENABLE(optimized-rtl,
-    AS_HELP_STRING([--enable-optimized-rtl],
-    ["Enable runtime library optimizations"]),
-    [OPTIMIZED_RTL="yes"],[OPTIMIZED_RTL="no"])
-
 #######################
 # Generating Makefile #
 #######################
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 995c81193f63cef84a73aea1defc830cec78fa27..80fca39458de1a608628d71c66c16330cd9fd065 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2016/08/02] Added --rt-debug feature to e-acsl-gcc.sh.
+	        --enable-optimized-rtl configure option removed
 -* E-ACSL       [2016/08/02] Added --enable-optimized-rtl option to configure
 -* E-ACSL       [2016/08/02] Removed --production|-P, --no-stdlib|-N and
 	        --debug-log|-D options of e-acsl-gcc.sh.
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index 60b1cad9c4505d45b3311d819b934e986a16c96d..6658f67ce76af7079293971c792354deddee0715 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -45,6 +45,10 @@ show a help page.
 compile the generated and the original (supplied) sources.
 By default no compilation is performed.
 .TP
+.B -D, --rt-debug
+Enable runtime debug features, i.e., compile unoptimized executable
+with assertions and extra checks.
+.TP
 .B -X, --instrumented-only
 Do not compile original code. Has effect only in the presence of the \fI-c\fP
 flag.
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
index fa4a92dbe1e991564dacefcd311f1bf73778d34e..b8229dd16473b656dd05835396ae46ae19904bc9 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -31,7 +31,7 @@ _eacsl_gcc() {
   opts="
     -i -C -p -d -o -O -v -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a
     -h -c -msegment -mbittree
-    --verbose= --debug= --debug-log= --logfile= --quiet --production --help
+    --verbose= --debug= --debug-log= --logfile= --quiet --rt-debug --help
     --ocode= --oexec= --oexec-e-acsl=
     --ld-flags= --cpp-flags= --extra-cpp-args=
     --frama-c-extra= --frama-c= --gcc= --e-acsl-share= --memory-model=
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 11b6bb946df17310183c6984f694c897b436f7ba..4ea21de6f5efe6f9e5efdbc6435afddffa90ba0f 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -125,17 +125,22 @@ rte_options() {
 #    model. In this case the following function prints the full path to a static
 #    library representing this memory model.
 mmodel_lib() {
-  local models="$(find $LIBDIR/ -name 'libeacsl-*-rtl.a' -exec basename {} \; \
-    | sed 's/^libeacsl-\(.*\)-rtl.a/\1/')"
+  local rt_feature="opt"
+  if [ -n "$OPTION_RT_DEBUG" ]; then
+    rt_feature="debug"
+  fi
+
+  local models="$(find $LIBDIR/ -name 'libeacsl-*-rtl-opt.a' -exec basename {} \; \
+    | sed 's/^libeacsl-\(.*\)-rtl-opt.a/\1/')"
 
   if [ -n "$1" ]; then
     local modelname="$(echo $models | tr ' ' '\n' | grep "^$1$")"
-    local modelpath="$(realpath $LIBDIR/libeacsl-$modelname-rtl.a 2>/dev/null)"
+    local modelpath="$(realpath $LIBDIR/libeacsl-$modelname-rtl-$rt_feature.a 2>/dev/null)"
 
     if [ -n "$modelpath" ]; then
       echo $modelpath
     else
-      error "Memory model '$1' is not available in this distribution"
+      error "Memory model '$1'-$rt_feature is not available in this distribution"
     fi
   else
     echo $models
@@ -151,8 +156,8 @@ LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:,
   frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
   ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,
   frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,
-  print-mmodels"
-SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,I:,G:,X,a:"
+  print-mmodels,rt-debug"
+SHORTOPTIONS="h,c,C,p,d:,D,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,I:,G:,X,a:"
 # Prefix for an error message due to wrong arguments
 ERROR="ERROR parsing arguments:"
 
@@ -168,6 +173,7 @@ OPTION_PRINT=                            # Output instrumented code
 OPTION_DEBUG=                            # Set Frama-C debug flag
 OPTION_VERBOSE=                          # Set Frama-C verbose flag
 OPTION_COMPILE=                          # Compile instrumented program
+OPTION_RT_DEBUG=                         # Enable runtime debug features
 OPTION_OUTPUT_CODE="a.out.frama.c"       # Name of the translated file
 OPTION_OUTPUT_EXEC="a.out"               # Generated executable name
 OPTION_EACSL_OUTPUT_EXEC=""              # Name of E-ACSL executable
@@ -246,6 +252,12 @@ do
       exec 2> $1
       shift;
     ;;
+    # Enable runtime debug features, i.e., compile unoptimized executable
+    # with assertions, extra checks and other debug features
+    --rt-debug|-D)
+      shift
+      OPTION_RT_DEBUG=1
+    ;;
     # Pass an option to a Frama-C invocation
     --frama-c-extra|-F)
       shift;
diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh
index 3158d01f55993e95b4fad7c92741c86b12f19fac..1365313c02e834d3813ffaaf876b0ec064d0d2c9 100755
--- a/src/plugins/e-acsl/scripts/testrun.sh
+++ b/src/plugins/e-acsl/scripts/testrun.sh
@@ -132,9 +132,10 @@ run_test() {
 
   # Compile instrumented source and run executable
   for model in $MODELS; do
-    # Command for compiling the instrumented file with a given memory model
-    COMMAND="$EACSLGCC --compile-only --memory-model=$model --logfile=$logfile \
-      --oexec-e-acsl=$oexec-$model $ocode"
+    # Command for compiling the instrumented file with a given memory model.
+    # Make sure executables are compiled in the debug mode.
+    COMMAND="$EACSLGCC --compile-only --rt-debug --memory-model=$model \
+      --logfile=$logfile --oexec-e-acsl=$oexec-$model $ocode"
     debug "Run $COMMAND"
     $COMMAND || error "Command $COMMAND failed" "$logfile"
     run_executable $oexec-$model $oexeclog-$model $model