diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf
index 6a57d1052d16a2618c4f9e470deca2c1db67668c..1361ba0bc29212571488c2a551fd1e1a0d6c31e5 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf differ
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 4b17d0b63eeeeb498581f9c4d9e8996406f7ade4..53e88a457e460537635be6a15eda367507e5495d 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -1,13 +1,13 @@
 MAIN=main
 
-C_CODE=first.i
+C_CODE=$(wildcard examples/*.[ci])
 
 DEPS_MODERN=eacslversion.tex biblio.bib macros.tex \
 	introduction.tex \
 	provides.tex \
 	limitations.tex \
 	changes.tex \
-	$(addprefix examples/, $(C_CODE))
+	$(C_CODE)
 
 
 default: main.pdf
diff --git a/src/plugins/e-acsl/doc/userman/examples/rte.i b/src/plugins/e-acsl/doc/userman/examples/rte.i
index 35536f6c5fb3afc1342d65953fddcf69e8bed9c7..9fa070ccad279c59032ba229f5c54d8e84fbbb6a 100644
--- a/src/plugins/e-acsl/doc/userman/examples/rte.i
+++ b/src/plugins/e-acsl/doc/userman/examples/rte.i
@@ -4,11 +4,11 @@
     behavior no:
      assumes x % y != 0;
      ensures \result == 0; */
-int divide(int x, int y) {
+int is_dividable(int x, int y) {
   return x % y == 0;
 }
 
 int main(void) {
-  divide(2, 0);
+  is_dividable(2, 0);
   return 0;
 }
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index 6a57d1052d16a2618c4f9e470deca2c1db67668c..1361ba0bc29212571488c2a551fd1e1a0d6c31e5 100644
Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and b/src/plugins/e-acsl/doc/userman/main.pdf differ