diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 74a0fbf809258e9993139a6ea8b8ca1d123a3111..a20ffddc2b30730ce849758bfc31d15497152d4c 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -167,14 +167,31 @@ $(EACSL_JEMALLOC_LIB):
 	$(MKDIR) $(EACSL_LIBDIR)
 	$(CP) $(EACSL_JEMALLOC_DIR)/lib/$(EACSL_JEMALLOC_LIBNAME) $@
 
-EACSL_GMP_DIR := $(PLUGIN_DIR)/contrib/libgmp
+
 EACSL_GMP_LIBNAME = libgmp-e-acsl.a
 EACSL_GMP_LIB = $(EACSL_LIBDIR)/$(EACSL_GMP_LIBNAME)
+EACSL_GMP_DIR := $(PLUGIN_DIR)/contrib/libgmp
+EACSL_GMP_MINI = mini-gmp.o
 
+ifeq (@FULL_GMP@, no)
+############
+# Mini GMP #
+############
+$(EACSL_GMP_LIB): $(EACSL_GMP_DIR)/mini-gmp/mini-gmp.c
+	echo 'CC          $< '
+	$(CC) $< -c -O2 -g3 -o$(EACSL_GMP_MINI)
+	echo 'AR          $@'
+	$(AR) crus $(EACSL_GMP_LIB) $(EACSL_GMP_MINI)
+	ranlib $(EACSL_GMP_LIB)
+else
+############
+# Full GMP #
+############
 $(EACSL_GMP_LIB):
 	cd $(EACSL_GMP_DIR) && ./configure && $(MAKE) $(MAKEOPTS)
 	$(MKDIR) $(EACSL_LIBDIR)
 	$(CP) $(EACSL_GMP_DIR)/.libs/libgmp.a $@
+endif
 
 all:: $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
 
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index 9424a1e4eaea85ce4541805b55c6e8b075d26bec..dd8cb6c01ca0ee45e69e0ac6a90154332ad5fe18 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -103,11 +103,19 @@ AC_CHECK_PROG(DOXYGEN,doxygen,doxygen,no)
 AC_CHECK_PROG(HAVE_DOT,dot,yes,no)
 AC_OUTPUT(PLUGIN_RELATIVE_PATH(doc/doxygen/doxygen.cfg), [  ])
 
+# GMP
+#####
+AC_ARG_ENABLE(full-gmp,
+    AS_HELP_STRING([--enable-full-gmp],
+    ["Disable runtime assertions in the RTL"]),
+    [FULL_GMP="yes"],[FULL_GMP="no"])
+
 #######################
 # Generating Makefile #
 #######################
 
 AC_SUBST(MAY_RUN_TESTS)
 AC_SUBST(OCAMLVERSION)
+AC_SUBST(FULL_GMP)
 
 write_plugin_config(Makefile)