diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 9a34457a9509d18e807cda747a15348b08e09ab5..3a354f53d22e625f8aaac97f115250c88e257df9 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2017/03/03] Remove precond rte option from e-acsl-gss.sh
 -* E-ACSL       [2017/03/02] Fix bts #1740 about incorrect monitoring of
 	        memory properties when early exiting a block through
 	        goto, break or continue.
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 81004e21e0762cb53d666abbc9fb38d3e7bef2f5..560f0a1563b79b469f87fe916b7776f5979230b5 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -132,7 +132,6 @@ Valid arguments are:
   \fImem\fP               \- pointer or array accesses.
   \fIfloat-to-int\fP      \- casts from floating-point to integer.
   \fIdiv\fP               \- division by zero.
-  \fIprecond\fP           \- function calls based on contracts.
   \fIshift\fP             \- left and right shifts by a value out of bounds.
   \fpointer-call\fP       \- annotate functions calls through pointers.
   \fIall\fP               \- all of the above.
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index dc17997f71ed14a242fb7423d97bed41ba525956..e8ca2cf350f87b6b6de62de926feedc2ac7c9163 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -97,8 +97,11 @@ rte_options() {
   local fc_options="signed-overflow unsigned-overflow \
     signed-downcast unsigned-downcast"
   # RTE assertions
-  local rte_options="div float-to-int mem pointer-call precond shift  \
+  local rte_options="div float-to-int mem pointer-call shift \
     trivial-annotations"
+  # Option supported by RTE but unsupported in E-ACSL, should
+  # always be negated
+  local rte_options_unsupported="precond"
   local generated="-rte" # Generated Frama-C options
 
   # Clean-up option strings
@@ -130,7 +133,7 @@ rte_options() {
     done
 
     # Generate assertion options for RTE (i.e., -rte-* or -rte-no-*)
-    for opt in $rte_options; do
+    for opt in $rte_options $rte_options_unsupported; do
       has_token $opt $asserts && prefix="-rte" || prefix="-rte-no"
       generated="$generated $prefix-$opt"
     done