diff --git a/Makefile b/Makefile
index fc166f543..182b6ff8e 100644
--- a/Makefile
+++ b/Makefile
@@ -160,7 +160,7 @@ doc: odoc sphinx-doc
 sphinx-doc:
 	# cp LICENSE.md $(SPHINX_DOC_DIR)/About/license.md
 	# cp -r licenses $(SPHINX_DOC_DIR)/About
-	$(SPHINXBUILD) "$(SPHINX_DOC_DIR)" "$(SPHINX_BUILD_DIR)"
+	$(SPHINXBUILD) -W "$(SPHINX_DOC_DIR)" "$(SPHINX_BUILD_DIR)"
 
 # Build the odoc
 odoc:
diff --git a/docs/sphinx_docs/Install/index.md b/docs/sphinx_docs/Install/index.md
index 68d8b6259..96b5d173d 100644
--- a/docs/sphinx_docs/Install/index.md
+++ b/docs/sphinx_docs/Install/index.md
@@ -3,7 +3,7 @@
 ## From a package manager
 
 Alt-ergo is available on [opam], the ocaml package manager with the following command :
-```
+```console
 opam install alt-ergo
 ```
 
@@ -29,33 +29,36 @@ External dependencies graph generated with `dune-deps` (use `make archi` for sou
 To compile the sources of the library `alt-ergo-lib` and the binary `alt-ergo`, you will need the
 following libraries :
 ```
-  ocaml >= 4.08.0
+  ocaml >= 4.08.1
   dune >= 3.0
   dune-build-info
-  dolmen >= 0.9
-  dolmen_loop >= 0.9
-  ocplib-simplex >= 0.5
-  zarith >= 1.4
+  dune-site
+  dolmen >= 0.10
+  dolmen_type >= 0.10
+  dolmen_loop >= 0.10
+  ocplib-simplex >= 0.5.1
+  zarith >= 1.11
   seq
-  fmt
-  ppx_blob
+  fmt >= 0.9.0
+  ppx_blob >= 0.7.2
   camlzip >= 1.07
   menhir
   dune-site
-  cmdliner
+  cmdliner >= 1.1.0
   psmt2-frontend >= 0.4
   stdlib-shims
+  ppx_deriving
 ```
 
 You can install dependencies using:
 
-```
+```console
 $ make deps
 ```
 
 and create a development switch with:
 
-```
+```console
 $ make dev-switch
 ```
 
@@ -104,8 +107,8 @@ $ make js-deps
 
 For this build rule you will need the following aditional libraries :
 ```
-js_of_ocaml between 4.0.1 and 5.0.1
-zarith_stubs_js
+js_of_ocaml >= 5.4.0
+zarith_stubs_js >= v0.16.1
 ```
 
 #### Alt-Ergo web worker
@@ -114,9 +117,9 @@ zarith_stubs_js
 
 For this build rule you will need the following aditional libraries :
 ```
-js_of_ocaml between 4.0.1 and 5.0.1
+js_of_ocaml >= 5.4.0
 js_of_ocaml-lwt
-zarith_stubs_js
+zarith_stubs_js >= v0.16.1
 data-encoding
 ```
 
@@ -128,11 +131,11 @@ This command create a `www/` directory in which you can find a small js example
 
 For this build rule you will need the following aditional libraries :
 ```
-js_of_ocaml between 4.0.1 and 5.0.1
+js_of_ocaml >= 5.4.0
 js_of_ocaml-lwt
 js_of_ocaml-ppx
 lwt_ppx
-zarith_stubs_js
+zarith_stubs_js >= v0.16.1
 data-encoding
 ```
 
diff --git a/docs/sphinx_docs/Model_generation.md b/docs/sphinx_docs/Model_generation.md
index a7f2c8694..a6098dd75 100644
--- a/docs/sphinx_docs/Model_generation.md
+++ b/docs/sphinx_docs/Model_generation.md
@@ -63,7 +63,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
   - Using the native language in the input file `INPUT.ae`:
 
-  ```
+  ```smt-lib
     logic a, b, c : int
     axiom A : a <> c
 
@@ -101,7 +101,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
   - Using the SMT-LIB language in the input file `INPUT.smt2`:
 
-  ```
+  ```smt-lib
     (set-logic ALL)
     (declare-fun a () Int)
     (declare-fun b () Int)
@@ -116,7 +116,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
   ```
   and the command `alt-ergo --produce-models INPUT.smt2` produces the output
-  ```
+  ```smt-lib
     unknown
     (
       (define-fun a () Int 0)
@@ -135,7 +135,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
 
   - Alternatively, using the statement `(set-option :produce-models true)`
-  ```
+  ```smt-lib
    (set-logic ALL)
    (set-option :produce-models true)
    (declare-fun a () Int)
@@ -149,7 +149,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   ```
   and the command `alt-ergo INPUT.smt2` produces
   the output model
-  ```
+  ```smt-lib
   unknown
   (
     (define-fun a () Int 0)
@@ -168,7 +168,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   done
   ```
   we got the SMT-LIB file `INPUT.smt2`:
-  ```
+  ```smt-lib
   (set-logic ALL)
   (declare-const i Int)
   (assert (and (< i 5) (not (< (+ i 1) 5))))
@@ -176,11 +176,11 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   (get-model)
   ```
   Execute the command
-  ```sh
+  ```console
   alt-ergo --produce-models INPUT.smt2
   ```
   We got the output
-  ```
+  ```smt-lib
   ; File "INPUT.smt2", line 4, characters 1-12: I don't know (0.6689) (2 steps) (goal g_1)
 
   unknown
@@ -199,7 +199,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   end
   ```
   and fix our SMT-LIB input accordingly:
-  ```
+  ```smt-lib
   (set-logic ALL)
   (declare-const i Int)
   (assert (and (< i 5) (not (<= (+ i 1) 5))))
@@ -214,20 +214,3 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   (error "No model produced.")
   ```
   Our invariant is valid!
-
-### Output
-The results of an Alt-ergo's execution have the following form :
-```
-File "<path_to_file>/<filename>", line <l>, characters <n-m>: <status> (<time in seconde>) (<number of steps> steps) (goal <name of the goal>)
-```
-The status can be `Valid`, `Invalid` or `I don't know`. If the input file is in
-the SMT-LIB 2 format the status will be either `unsat`, `sat`, `unknown`.
-You can force the status to be print in the SMT-LIB 2 form with the option `--output smtlib2`.
-
-```{admonition} Note
-When Alt-Ergo tries to prove a `goal` (with the native input language), it
-actually tries to prove the unsatisfiability of its negation. That is
-why you get `unsat` answer as an SMT-LIB 2 format output while proving a `Valid`
-goal. The same goes for `Invalid` and `sat`.
-```
-
diff --git a/docs/sphinx_docs/Optimization.md b/docs/sphinx_docs/Optimization.md
new file mode 100644
index 000000000..0ed636598
--- /dev/null
+++ b/docs/sphinx_docs/Optimization.md
@@ -0,0 +1,104 @@
+# Optimization
+
+Since version 2.6.0, Alt-Ergo supports optimization for LIA and Bitvector
+theories.
+
+## MaxSMT syntax
+
+- Use `(maximize ...)` and `(minimize ...)` statements to specify an objective function.
+
+- Use `(get-objectives)` after `(check-sat)` to output the best values
+  for each objective function.
+
+## Activation
+
+You only need to [enable model generation](Model_generation.md#activation).
+The identifiers `maximize`, `minimize` and `get-objectives` are reserved by
+default. If you want to disable the `MaxSMT` extension, use the
+[strict mode](Usage/index.md#strict-mode).
+
+```{admonition} Note
+The optimization feature is only compatible with the SAT solver `CDCL-Tableaux`,
+which is the default.
+```
+
+## Examples
+
+First, consider a classical linear programming problem:
+```smt-lib
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= (+ (* 5 x) (* 2 y) (* (- 0 3) z)) 25))
+(assert (= (+ (* (- 0 2) x) (* 4 y)) 8))
+(assert (<= x y))
+(maximize x)
+(check-sat)
+(get-model)
+(get-objectives)
+```
+Alt-Ergo outputs:
+```smt-lib
+unknown
+(
+  (define-fun x () Int 4)
+  (define-fun y () Int 4)
+  (define-fun z () Int 1)
+)
+(objectives
+  (x 4)
+)
+```
+
+- The optimization also works with an expression in `maximize`:
+```smt-lib
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(assert (<= x 5))
+(assert (<= 0 y))
+(maximize (- (* 5 x) y))
+(check-sat)
+(get-objectives)
+```
+Alt-Ergo outputs:
+```smt-lib
+unknown
+(
+  (define-fun x () Int 5)
+  (define-fun y () Int 0)
+)
+(objectives
+  ((- (* 5 x) y) 25)
+)
+```
+
+- Finally, an example with bitvectors:
+```smt-lib
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x (_ BitVec 32))
+(declare-const y (_ BitVec 32))
+(assert (bvult x (_ bv2 32)))
+(assert (bvule y (_ bv10 32)))
+(maximize x)
+(maximize y)
+(check-sat)
+(get-model)
+(get-objectives)
+```
+Alt-Ergo outputs:
+```smt-lib
+unknown
+(
+  (define-fun x () (_ BitVec 32) #x00000001)
+  (define-fun y () (_ BitVec 32) #x0000000a)
+)
+(objectives
+  (x #x00000001)
+  (y #x0000000a)
+)
+```
diff --git a/docs/sphinx_docs/Plugins/ab_why3.md b/docs/sphinx_docs/Plugins/ab_why3.md
index 64d75552e..bde7b6868 100644
--- a/docs/sphinx_docs/Plugins/ab_why3.md
+++ b/docs/sphinx_docs/Plugins/ab_why3.md
@@ -25,7 +25,7 @@ prove the goals given in a file `b-why3-POs.ae` with the following
 command:
 
 
-```
+```console
  ./alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
 ```
 
@@ -37,7 +37,7 @@ theory for Alt-Ergo.
 For instance, using the following command to prove the goals in the
 file `examples/AB-Why3-plugin/p4_34.why.zip`:
 
-```
+```console
 ./alt-ergo examples/AB-Why3-plugin/p4_34.why.zip --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae  --timelimit-per-goal --timelimit 3 --no-locs-in-answers
 ```
 
@@ -57,7 +57,7 @@ Valid (0.0525) (215 steps) (goal g_5)
 If you have already installed this version of Alt-Ergo and this plugin, you should be able to simply use the command:
 
 
-```
+```console
  alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
 ```
 
diff --git a/docs/sphinx_docs/Plugins/index.md b/docs/sphinx_docs/Plugins/index.md
index 2b5e833fd..04c66dcab 100644
--- a/docs/sphinx_docs/Plugins/index.md
+++ b/docs/sphinx_docs/Plugins/index.md
@@ -13,7 +13,9 @@ The `fm-simplex` inequality plugin comes built-in with Alt-Ergo and no further
 installation is required. It is distributed under the same licensing conditions
 as Alt-Ergo. It can be used as follows:
 
-    $ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
+```console
+$ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
+```
 
 ```{note}
 If you are a developer of an external inequality plugin, your plugin needs to
diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md
index 586b7a570..58a41bfc4 100644
--- a/docs/sphinx_docs/Usage/index.md
+++ b/docs/sphinx_docs/Usage/index.md
@@ -4,18 +4,39 @@
 
 Alt-Ergo is executed with the following command:
 
-        $ alt-ergo   [options] file.<ext>
+```console
+$ alt-ergo   [options] file.<ext>
+```
 
 The CDCL solver is now the default SAT engine. The command below
 allows to enable the old Tableaux-like SAT-solver:
 
-        $ alt-ergo   [options] --sat-solver Tableaux file.<ext>
+```console
+$ alt-ergo   [options] --sat-solver Tableaux file.<ext>
+```
+
+### Output
+The results of an Alt-ergo's execution have the following form :
+```
+File "<path_to_file>/<filename>", line <l>, characters <n-m>: <status> (<time in seconde>) (<number of steps> steps) (goal <name of the goal>)
+```
+The status can be `Valid`, `Invalid` or `I don't know`. If the input file is in
+the SMT-LIB 2 format the status will be either `unsat`, `sat`, `unknown`.
+You can force the status to be print in the SMT-LIB 2 form with the option `--output smtlib2`.
+
+```{admonition} Note
+When Alt-Ergo tries to prove a `goal` (with the native input language), it
+actually tries to prove the unsatisfiability of its negation. That is
+why you get `unsat` answer as an SMT-LIB 2 format output while proving a `Valid`
+goal. The same goes for `Invalid` and `sat`.
+```
 
 ### Files extensions
 Alt-Ergo supports file extensions:
 - `.psmt2`, `.smt2` for (our polymorphic extension of) the SMT-LIB 2
   standard
 - `.ae`, for its native input language (`.why` and `.mlw` are now deprecated although still accepted)
+- `.psmt2.zip`, `.smt2.zip` and `.ae.zip` for compressed files
 
 See the [SMT-LIB language] and [Alt-ergo native language] sections for more information about the format of the input files.
 
@@ -41,7 +62,9 @@ SMT-LIB features will not work with the `legacy` frontend. Use the (default)
 
 Preludes can be passed to Alt-Ergo as follows:
 
-        $ alt-ergo --prelude p.ae --prelude some-path/q.ae [other-options] file.ae
+```console
+$ alt-ergo --prelude p.ae --prelude some-path/q.ae [other-options] file.ae
+```
 
    Alt-Ergo will try to load a local prelude called "p.ae". If this
    fails, Alt-Ergo tries to load it from the default preludes
@@ -49,6 +72,19 @@ Preludes can be passed to Alt-Ergo as follows:
    path). You can also provide a relative or an absolute path as shown
    by "some-path/q.ae".
 
+### Strict mode
+Alt-Ergo supports extensions that are not part of the SMT-LIB standard. For
+convenience, some of these extensions are enabled by default. Since the
+version 2.6.0, the flag `--strict` disables the extensions:
+- MaxSMT extension for the optimization
+
+We plan to disable more nonstandard extensions with this flag in futur versions.
+## Library
+
+Since version 2.2.0, Alt-Ergo's library is also compiled and installed. See the
+[API documentation] (also available [on ocaml.org](https://ocaml.org/p/alt-ergo-lib/latest/doc/index.html))
+for more information.
+
 ## Javascript
 
 Alt-Ergo can be compiled in Javascript see the [install section] for more informations.
@@ -57,7 +93,9 @@ Alt-Ergo can be compiled in Javascript see the [install section] for more inform
 
 The Javascript version of Alt-Ergo compatible with node-js is executed with the following command:
 
-        $ node alt-ergo.js  [options] file.<ext>
+```console
+$ node alt-ergo.js  [options] file.<ext>
+```
 
 Note that timeout options and zip files are not supported with this version because of the lack of js primitives.
 
@@ -105,12 +143,6 @@ Look at the `worker_json_example.json` in the ressources `rsc` of the project to
 
 A small example of how to use the Alt-Ergo web worker can be build with the command ```make js-example```. This command also makes the web worker if it has not already been built. It produces a `www` directory with an html page where you can write a small example, run the worker, and see the results. You can also look at the console of your browser to look at the json file sent
 
-## Library
-
-Since version 2.2.0, Alt-Ergo's library is also compiled and installed. See the
-[API documentation] (also available [on ocaml.org](https://ocaml.org/p/alt-ergo-lib/latest/doc/index.html))
-for more information.
-
 [install section]: ../Install/index.md
 [Lwt]: https://ocsigen.org/lwt/
 [js_of_ocaml]: https://ocsigen.org/js_of_ocaml/
diff --git a/docs/sphinx_docs/alt_ergo_lexer.py b/docs/sphinx_docs/alt_ergo_lexer.py
index 185883970..fce2bbb56 100644
--- a/docs/sphinx_docs/alt_ergo_lexer.py
+++ b/docs/sphinx_docs/alt_ergo_lexer.py
@@ -1,5 +1,6 @@
 from pygments.lexer import RegexLexer, include
-from pygments.token import *
+from pygments.token import String, Text, Name, Comment,\
+    Keyword, Operator, Number
 
 __globals__ = [ 'AltErgoLexer' ]
 
@@ -24,7 +25,7 @@ class AltErgoLexer(RegexLexer):
     keyopts = (
         r',', r';', r'\(', r'\)', r':', r'->', r'<-', r'<->', r'=', r'<', r'<=',
         r'>', r'>=', r'<>', r'\+', r'-', r'\*', r'\*\*', r'\*\*\.', r'/', r'%',
-        r'@', r'\.', r'#', r'\[', r'\]', r'\{', r'\}', 'r\|', r'\^', r'\|->',
+        r'@', r'\.', r'#', r'\[', r'\]', r'\{', r'\}', r'\|', r'\^', r'\|->',
     )
 
     word_operators = ('and', 'in', 'or', 'xor')
diff --git a/docs/sphinx_docs/conf.py b/docs/sphinx_docs/conf.py
index bc9dc97d9..ec9617561 100644
--- a/docs/sphinx_docs/conf.py
+++ b/docs/sphinx_docs/conf.py
@@ -17,7 +17,7 @@
 
 # -- Project information -----------------------------------------------------
 
-project = 'Alt-Ergo'
+project = 'Alt-Ergo Documentation'
 copyright = '2020 - 2023, Alt-Ergo developers'
 author = 'Alt-Ergo developers'
 
@@ -42,7 +42,7 @@
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
-extensions = ['myst_parser', 'sphinx_markdown_tables']
+extensions = ['myst_parser']
 
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']
@@ -57,7 +57,10 @@
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
 #
-html_theme = 'furo'
+html_theme = 'sphinx_rtd_theme'
+html_theme_options = {
+  'navigation_depth': 5,
+}
 
 # -- Options for MyST markdown parser ----------------------------------------
 
diff --git a/docs/sphinx_docs/index.md b/docs/sphinx_docs/index.md
index 52d7d6a47..cf24b3289 100644
--- a/docs/sphinx_docs/index.md
+++ b/docs/sphinx_docs/index.md
@@ -16,8 +16,8 @@ If you are using Alt-Ergo as a library, see the [API documentation](API/index) (
 Alt-ergo supports different input languages:
 
 - Alt-ergo supports the SMT-LIB language v2.6. **This is Alt-Ergo's preferred
-  and recommended input format.** 
-- The original input language is its native language, based on the language of the Why3 platform.
+  and recommended input format.**
+- The original input language is its native language, based on the language of the Why3 platform. Since the version 2.6.0, this language is deprecated.
 - It also (partially) supports the input language of Why3 through the [AB-Why3 plugin](../Plugins/ab_why3).
 
 ```{toctree}
@@ -29,6 +29,7 @@ Usage                      <Usage/index>
 SMT-LIB language           <SMT-LIB_language/index>
 Alt-Ergo's native language <Alt_ergo_native/index>
 Model generation           <Model_generation>
+Optimization               <Optimization>
 API documentation          <API/index>
 Plugins                    <Plugins/index>
 Developer's documentation  <Dev/index>
diff --git a/docs/sphinx_docs/requirements.txt b/docs/sphinx_docs/requirements.txt
index a733578c0..11c0472ab 100644
--- a/docs/sphinx_docs/requirements.txt
+++ b/docs/sphinx_docs/requirements.txt
@@ -4,6 +4,5 @@
 ###### Requirements for sphinx doc ######
 sphinx >= 4.4.0
 myst-parser
-furo
-sphinx-markdown-tables
+sphinx_rtd_theme
 #
diff --git a/nix/default.nix b/nix/default.nix
index 00ee3ecf9..7742f9083 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -12,7 +12,6 @@ import sources.nixpkgs {
         dolmen_loop = pkgs.callPackage ./dolmen_loop.nix { };
         landmarks = pkgs.callPackage ./landmarks.nix { };
         landmarks-ppx = pkgs.callPackage ./landmarks-ppx.nix { };
-        furo = pkgs.callPackage ./furo.nix { };
       });
     })
   ];
diff --git a/shell.nix b/shell.nix
index 1c4f80e07..d5deacf49 100644
--- a/shell.nix
+++ b/shell.nix
@@ -12,8 +12,7 @@ pkgs.mkShell {
     pkgs.ocamlformat
     pkgs.sphinx
     python3Packages.myst-parser
-    python3Packages.sphinx-markdown-tables
-    python3Packages.furo
+    python3Packages.sphinx-rtd-theme
     ocaml
     dune_3
     ocaml-lsp