diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md
index 646c41df8f..6867fe1890 100644
--- a/docs/sphinx_docs/Usage/index.md
+++ b/docs/sphinx_docs/Usage/index.md
@@ -238,16 +238,10 @@ See the [AB-Why3 README] file for the documentation of the AB-Why3 plugin
 
 The Fm-Simplex plugin can be used as follows:
 
-        $ alt-ergo --inequalities-plugin fm-simplex-plugin.cmxs [other-options] file.<ext>
-        $ alt-ergo --inequalities-plugin some-path/fm-simplex-plugin.cmxs [other-options] file.<ext>
+        $ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
 
-   Alt-Ergo will try to load a local plugin called
-   "fm-simplex-plugin.cmxs". If this fails, Alt-Ergo tries to load it
-   from the default plugins directory (run `alt-ergo --where plugins`
-   to see its absolute path). You can also provide a relative or an
-   absolute path as shown by the second command above. Also, you
-   should replace ".cmxs" by ".cma" if you are working with bytcode
-   binaries.
+The inequalities plugins are [Dune-site plugins] registered in the `(alt-ergo
+plugins)` site. The `fm-simplex` plugin comes built-in with Alt-Ergo.
 
 ### Preludes
 
@@ -339,3 +333,4 @@ A small example of how to use the Alt-Ergo web worker can be build with the comm
 [API documentation]: ../API/index.md
 [AB-Why3 README]: ../Plugins/ab_why3.md
 [Input section]: ../Input_file_formats/index
+[Dune-site plugins]: https://dune.readthedocs.io/en/stable/sites.html#plugins
diff --git a/src/bin/common/config.ml b/src/bin/common/config.ml
index 5e1e7df1cd..aa28b95334 100644
--- a/src/bin/common/config.ml
+++ b/src/bin/common/config.ml
@@ -20,3 +20,14 @@ let lookup_file locations filename =
 let lookup_prelude = lookup_file preludes_locations
 
 let lookup_plugin = lookup_file plugins_locations
+
+let load_plugin plugin =
+  try
+    AltErgoSites.Plugins.Plugins.load plugin
+  with e ->
+    AltErgoLib.Errors.run_error
+      (Dynlink_error
+         (Format.asprintf
+            "@[<v>Loading the plugin %S failed!@,\
+             >> Failure message: %s"
+            plugin (Printexc.to_string e)))
diff --git a/src/bin/common/dune b/src/bin/common/dune
index 9c56361e41..307f982a50 100644
--- a/src/bin/common/dune
+++ b/src/bin/common/dune
@@ -12,6 +12,7 @@
    stdlib-shims
    cmdliner
    dune-site
+   dune-site.plugins
  )
  (modules
    Config
@@ -25,4 +26,6 @@
 
 (generate_sites_module
  (module AltErgoSites)
- (sites alt-ergo))
+ (sites alt-ergo)
+ (plugins
+  (alt-ergo plugins)))
diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index f004be9ca6..05762cd93a 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -1310,12 +1310,14 @@ let parse_theory_opt =
       | "" ->
         if debug then
           Printer.print_dbg
-            "[Dynlink] Using the 'FM module' for arithmetic inequalities";
+            "Using the 'FM module' for arithmetic inequalities";
         Ok ()
       | path ->
         try
-          MyDynlink.load debug path
-            "'inequalities' reasoner (FM module)";
+          Config.load_plugin path;
+          if debug then
+            Printer.print_dbg
+              "Using the 'inequalities' reasoner (FM module) %S" path;
           Ok ()
         with Errors.Error e ->
           Error (Format.asprintf "%a" Errors.report e)
diff --git a/src/plugins/fm-simplex/dune b/src/plugins/fm-simplex/dune
index e257fd5b83..e1adea3906 100644
--- a/src/plugins/fm-simplex/dune
+++ b/src/plugins/fm-simplex/dune
@@ -3,13 +3,13 @@
   (mld_files :standard))
 
 (library
+ (public_name alt-ergo.plugins.fm-simplex)
  (name FmSimplexPlugin)
  (libraries alt-ergo-lib)
  (modules Simplex Simplex_cache FmSimplexIneqs))
 
-(install
+(plugin
  (package alt-ergo)
- (section (site (alt-ergo plugins)))
- (files
-  FmSimplexPlugin.cma
-  FmSimplexPlugin.cmxs))
+ (name fm-simplex)
+ (libraries alt-ergo.plugins.fm-simplex)
+ (site (alt-ergo plugins)))
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index c5c560aab4..ff4214ec69 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -1,6 +1,5 @@
-  $ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -E 's/\(\\".*\\"\)//'
-  alt-ergo: Fatal Error: [Dynlink] Loading the 'inequalities' reasoner (FM module) plugin in "does-not-exist" failed!
-            >> Failure message: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure")
+  $ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -e '/^[[:space:]]*>>/d'
+  alt-ergo: Fatal Error: [Dynlink] Loading the plugin "does-not-exist" failed!
 
 Now we will have some tests for the models. Note that it is okay if the format
 changes slightly, you should be concerned with ensuring the semantic is