diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 9e76ca9766fd1fac7a0854fad0129b8268afd1e5..77837f8be73f939ad96d77971a8ec1ad7d469ad3 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -198,11 +198,9 @@ MKRTL = \
   object=$$(basename -s .a $2).o && \
   echo ' CC $3' && \
   $(CC) $1 -c -o$$object $3 && \
-  (cd $(EACSL_LIBDIR) && $(AR) -x $(EACSL_GMP_LIBNAME)) && \
-  (cd $(EACSL_LIBDIR) && $(AR) -x $(EACSL_JEMALLOC_LIBNAME)) && \
   echo ' AR $2' && \
-  $(AR) crus $2 $$object $(EACSL_LIBDIR)/*.o && \
-  $(RM) -f $$object $(EACSL_LIBDIR)/*.o && \
+  $(AR) crus $2 $$object && \
+  $(RM) -f $$object && \
   ranlib $2
 
 $(EACSL_LIBDIR)/libeacsl-rtl-%.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC) $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 934325005ecf522ec30da5ad6275465a91f1f030..92dcc8cd6ba4bfc36ce4e6181c3d1d5995ce95be 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -126,7 +126,8 @@ runtime can be generated using a \C compiler (for instance \gcc), as follows:
 
 \lstset{escapechar=£}
 \begin{shell}
-\$ gcc monitored_first.i -omonitored_first -leacsl-rtl-bittree -lpthread -lm
+\$ gcc monitored_first.i -omonitored_first \
+  -leacsl-rtl-bittree -leacsl-gmp -leacsl-jemalloc -lpthread -lm
 monitored_first.i:9:1: warning: '__FC_BUILTIN__' attribute directive ignored [-Wattributes]
  typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
  ^
@@ -142,9 +143,15 @@ The displayed warnings can be safely ignored as they refer to the attribute
 using \shortopt{Wno-attributes} \gcc option. You may also notice that the
 generated executable (\texttt{monitored\_first}) is linked against the \eacsl
 static library (i.e., via \texttt{-leacsl-rtl-bittree}) installed alongside the
-\eacsl plug-in. This library provides definitions of the functions used by
-\eacsl during its runtime analysis.
-We describe libraries used by \eacsl later on in Section~\ref{sec:memory}.
+\eacsl plug-in.  This library provides definitions of the functions used by
+\eacsl during its runtime analysis.  The monitored executable is also linked
+against the customized versions of the \jemalloc memory allocator
+(\T{-leacsl-jemalloc}) and the \gmp library (\T{-leacsl-gmp}) used by \eacsl.
+Even though in this example they are not strictly needed (since the transformed
+executable neither tracks memory nor reasons about arbitrary precision
+integers) we show all libraries potentially used by a transformed executable
+for completeness purposes.  We describe the libraries used by \eacsl later on
+in Section~\ref{sec:memory}.
 
 Finally you can execute the generated binary.
 \begin{shell}
@@ -543,14 +550,21 @@ The functionality of the provided memory models (and therefore libraries
 implementing them) is equivalent, however they differ in performance. We
 further discuss performance considerations.
 
-Additionally to memory tracking both libraries include customized version of
-the \gmp library, \jemalloc\footnote{\url{http://jemalloc.net/}} memory
-allocator replacing system-wide malloc and other utilities including \eacsl
-assertions.  It is therefore safe to link an \eacsl-instrumented program
-against any of these libraries.  For instance, in Section~\ref{sec:exec} we
-have linked the instrumented program in \texttt{monitored\_first.i} against
-\T{libeacsl-rtl-bittree.a}, but you can also link it against the library
-implementing the segment-based memory model via \T{-leacsl-rtl-segment}.
+Both libraries use the same API and differ only in implementation, therefore it
+is safe to link an \eacsl-instrumented program against any of these libraries.
+For instance, in Section~\ref{sec:exec} we have linked the instrumented program
+in \texttt{monitored\_first.i} against \T{libeacsl-rtl-bittree.a}, but you can
+also link it against the library implementing the segment-based memory model
+via \T{-leacsl-rtl-segment}.
+
+The \eacsl libraries allocate heap memory using a customized version of the
+\jemalloc\footnote{\url{http://jemalloc.net/}} memory allocator replacing
+system-wide \T{malloc} and similar functions (e.g., \T{calloc} or \T{free}).
+Mathematical integers used by \eacsl are implemented using a customized version
+of the \gmp library. Both, \jemalloc and \gmp should be added at link time as
+shown in Section~\ref{sec:exec}.  We, however, recommend using \eacslgcc who
+adds necessary compile- and link-time dependencies and allows for easy
+switching between different memory models as discussed  below.
 
 At the level of \eacslgcc you can choose between different memory models using
 the \shortopt{m} switch followed by the name of the memory model to link
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index bfde3a5c2404b10cd54b9909fe85a356705e9ea8..66c4149205fbd2be540216578299f981c48831e5 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -552,7 +552,7 @@ LDFLAGS="$OPTION_LDFLAGS"
 # C, CPP and LD flags for compilation of E-ACSL-generated sources
 EACSL_CFLAGS=""
 EACSL_CPPFLAGS="-I$EACSL_SHARE"
-EACSL_LDFLAGS="-lm -lpthread"
+EACSL_LDFLAGS="$LIBDIR/libeacsl-jemalloc.a $LIBDIR/libeacsl-gmp.a -lm -lpthread"
 
 # Output file names
 OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source