diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 91e71e2e0b2bc89095a3f3456eccb30ceb2ed17d..b149e813820494353d192aac49cd7efad09b86a0 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -116,7 +116,7 @@ ifeq (@MAY_RUN_TESTS@,yes)
 $(PLUGIN_DIR)/tests/print.cmxs: OFLAGS=-I $(FRAMAC_LIBDIR)
 $(PLUGIN_DIR)/tests/print.cmo: BFLAGS=-I $(FRAMAC_LIBDIR)
 
-PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime bts
+PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime bts gmp
 E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config \
 	$(PLUGIN_DIR)/tests/print.cmxs \
 	$(PLUGIN_DIR)/tests/print.cmo
diff --git a/src/plugins/e-acsl/tests/gmp/README.md b/src/plugins/e-acsl/tests/gmp/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..6ba931bda4209542e62d5c4a7f685296e0932d52
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/README.md
@@ -0,0 +1 @@
+Like e-acsl-runtime, but also test the -e-acsl-gmp-only mode.
diff --git a/src/plugins/e-acsl/tests/gmp/test_config b/src/plugins/e-acsl/tests/gmp/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..8ae28537c63f86a6461cac68f29c38c260b77e75
--- /dev/null
+++ b/src/plugins/e-acsl/tests/gmp/test_config
@@ -0,0 +1,4 @@
+LOG: gen_@PTEST_NAME@.c
+OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
+EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ gmp "" "--frama-c=@frama-c@"
+OPT: -check -e-acsl -e-acsl-gmp-only -then-last -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results