diff --git a/.github/workflows/documentation.yml b/.github/workflows/documentation.yml
index 58ea56154..fd27ea311 100644
--- a/.github/workflows/documentation.yml
+++ b/.github/workflows/documentation.yml
@@ -101,8 +101,10 @@ jobs:
         uses: ammaraskar/sphinx-action@master
         with:
           docs-folder: "docs/sphinx_docs/"
-          build-command: |
-            sphinx-build -b html -A current_version=${{ steps.version-name.outputs.target }} . _build
+          build-command: >
+            sphinx-build -W -b html
+              -A current_version=${{ steps.version-name.outputs.target }}
+              . _build
 
       # Create and upload an artifact `sphinx_doc` that contains the sphinx
       # documentation in html format.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 49a79b248..1662a7615 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -26,7 +26,7 @@ The following terms apply to all such contributions:
 
 In addition to agreeing to the terms of the Alt-Ergo's [License], we ask our contributors to sign the [Contributor License Agreement (CLA)].
 
-[License]: ../About/licenses/index
+[License]: ../About/license
 [Contributor License Agreement (CLA)]: https://www.ocamlpro.com/files/CLA-OCamlPro-corporate.txt
 
 ## Develop with Nix
diff --git a/docs/sphinx_docs/conf.py b/docs/sphinx_docs/conf.py
index b7fc87407..d7a305224 100644
--- a/docs/sphinx_docs/conf.py
+++ b/docs/sphinx_docs/conf.py
@@ -25,8 +25,10 @@
 
 # Import our custom lexer
 from alt_ergo_lexer import AltErgoLexer
+from smt_lib_lexer import Smt2Lexer
 from sphinx.highlighting import lexers
 lexers['alt-ergo'] = AltErgoLexer()
+lexers['smt-lib'] = Smt2Lexer()
 
 # Use alt-ergo as the default language
 highlight_language = 'alt-ergo'
diff --git a/docs/sphinx_docs/smt_lib_lexer.py b/docs/sphinx_docs/smt_lib_lexer.py
new file mode 100644
index 000000000..348f33d49
--- /dev/null
+++ b/docs/sphinx_docs/smt_lib_lexer.py
@@ -0,0 +1,89 @@
+from pygments.lexer import RegexLexer, words
+from pygments.token import *
+
+__globals__ = [ 'Smt2Lexer' ]
+
+class Smt2Lexer(RegexLexer):
+    """
+    A SMT-LIB lexer.
+    """
+    name = 'SMT-LIB'
+    url = 'https://smt-lib.org/'
+    aliases = [ 'smt2' ]
+    filenames = [ '*.smt2' ]
+    mimetypes = [ 'text/x-smt2 ']
+
+    keywords = (
+        # Commands
+        'assert', 'check-sat', 'check-sat-assuming', 'declare-const',
+        'declare-datatype', 'declare-datatypes', 'declare-fun',
+        'declare-sort', 'define-fun', 'define-fun-rec', 'define-funs-rec',
+        'define-sort', 'echo', 'exit', 'get-assertions', 'get-assignment',
+        'get-info', 'get-model', 'get-option', 'get-proof',
+        'get-unsat-assumptions', 'get-unsat-core', 'get-value', 'pop', 'push',
+        'reset', 'reset-assertions', 'set-info', 'set-logic', 'set-option',
+
+        # Term builtins
+        'let', 'forall', 'exists', 'match', '!', 'par', '_',
+    )
+
+    sorts = (
+        'Int', 'Bool', 'Real', 'BitVec', 'Array', 'RoundingMode',
+    )
+
+    builtins = (
+        # ArraysEx
+        'select', 'store',
+
+        # Bit-vectors
+        'concat', 'extract', 'bvnot', 'bvneg',
+        'bvand', 'bvor', 'bvxor', 'bvult', 'bvule', 'bvugt', 'bvuge',
+        'bvslt', 'bvsle', 'bvsgt', 'bvsge', 'bvadd', 'bvmul', 'bvudiv',
+        'bvsdiv', 'bvurem', 'bvsrem', 'bvshl', 'bvlshr', 'bvashr',
+        'bvnand', 'bvnor', 'bvxnor','bvsub', 'repeat', 'zero_extend',
+        'sign_extend', 'rotate_left', 'rotate_right',
+
+        # Core
+        'not', 'and', 'or', 'xor', 'distinct', 'ite',
+
+        # Ints, Reals and Reals_Ints
+        'div', 'mod', 'abs',
+        'to_real', 'to_int', 'is_int',
+
+        # Custom
+        'ae.round',
+        'ae.float16', 'ae.float32', 'ae.float64', 'ae.float128',
+    )
+
+    operators = (
+        '=>', '=', '-', '+', '*', '/', '<', '<=', '>', '>=',
+    )
+
+    symbol = r'(?:(?:[a-zA-Z0-9+/*=%?!.$_~&^<>@-]+)|(?:\|[^\|]+\|))'
+
+    symbol_suffix = r'(?![a-zA-Z0-9+/*=%?!.$_~&^<>@-])'
+
+    tokens = {
+        'root': [
+            (r';.*$', Comment.Single),
+            (r'\s+', Text),
+
+            (r'[0-9]+', Number.Integer),
+            (r'#x[0-9a-fA-F]+', Number.Integer.Hex),
+            (r'#b[0-1]+', Number.Integer.Bin),
+            (r'[0-9]+\.[0-9]+', Number.Float),
+            (r'"([^"]|"")*"', String),
+            (r':' + symbol, String.Symbol),
+
+            (r'true|false', Name.Constant),
+            (r'bv[0-9]+', Name.Constant),
+            (words(operators, suffix=symbol_suffix), Name.Operator),
+            (words(keywords, suffix=symbol_suffix), Keyword),
+            (words(sorts, suffix=symbol_suffix), Keyword.Type),
+            (words(builtins, suffix=symbol_suffix), Keyword.Builtin),
+
+            (symbol, Name),
+
+            (r'[_()]', Punctuation),
+        ],
+    }