diff --git a/.gitignore b/.gitignore
index 861c1cbc19..6a48d9cf7e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -41,5 +41,8 @@ alt-ergo.js
 alt-ergo-worker.js
 www/
 
+# Generated python files
+__pycache__
+
 # Generated nix files
 /result*
diff --git a/docs/sphinx_docs/alt_ergo_lexer.py b/docs/sphinx_docs/alt_ergo_lexer.py
new file mode 100644
index 0000000000..185883970d
--- /dev/null
+++ b/docs/sphinx_docs/alt_ergo_lexer.py
@@ -0,0 +1,72 @@
+from pygments.lexer import RegexLexer, include
+from pygments.token import *
+
+__globals__ = [ 'AltErgoLexer' ]
+
+class AltErgoLexer(RegexLexer):
+    """
+    For the Alt-Ergo language.
+    """
+
+    name = 'Alt-Ergo'
+    url = 'https://alt-ergo.ocamlpro.com/'
+    aliases = ['alt-ergo']
+    filenames = ['*.ae']
+    mimetypes = ['text/x-alt-ergo']
+
+    keywords = (
+        'ac', 'axiom', 'bitv', 'case_split', 'check', 'cut',
+        'distinct', 'else', 'end', 'exists', 'extends', 'forall',
+        'function', 'goal', 'check_sat', 'if', 'let', 'logic', 'not',
+        'predicate', 'prop', 'rewriting', 'then', 'theory',
+        'type', 'match', 'with', 'of',
+    )
+    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'\|->',
+    )
+
+    word_operators = ('and', 'in', 'or', 'xor')
+    primitives = ('bool', 'int', 'real', 'unit', 'void')
+
+    tokens = {
+        'escape-sequence': [
+            (r'\\[\\"\'ntbr]', String.Escape),
+            (r'\\[0-9]{3}', String.Escape),
+            (r'\\x[0-9a-fA-F]{2}', String.Escape),
+        ],
+        'root': [
+            (r'\s+', Text),
+            (r'false|true', Name.Builtin.Pseudo),
+            (r'\(\*(?![)])', Comment, 'comment'),
+            (r'\b(%s)\b' % '|'.join(keywords), Keyword),
+            (r'(%s)' % '|'.join(keyopts[::-1]), Operator),
+            (r'\b(%s)\b' % '|'.join(word_operators), Operator.Word),
+            (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type),
+
+            (r"\??[^\W\d][\w?']*", Name),
+
+            (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float),
+            (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex),
+            (r'0[oO][0-7][0-7_]*', Number.Oct),
+            (r'0[bB][01][01_]*', Number.Bin),
+            (r'\d[\d_]*', Number.Integer),
+
+            (r"'", Keyword),
+
+            (r'"', String.Double, 'string'),
+        ],
+        'comment': [
+            (r'[^(*)]+', Comment),
+            (r'\(\*', Comment, '#push'),
+            (r'\*\)', Comment, '#pop'),
+            (r'[(*)]', Comment),
+        ],
+        'string': [
+            (r'[^\\"]+', String.Double),
+            include('escape-sequence'),
+            (r'\\\n', String.Double),
+            (r'"', String.Double, '#pop'),
+        ],
+    }
diff --git a/docs/sphinx_docs/conf.py b/docs/sphinx_docs/conf.py
index cf504c2a31..8dd321104d 100644
--- a/docs/sphinx_docs/conf.py
+++ b/docs/sphinx_docs/conf.py
@@ -9,10 +9,10 @@
 # If extensions (or modules to document with autodoc) are in another directory,
 # add these directories to sys.path here. If the directory is relative to the
 # documentation root, use os.path.abspath to make it absolute, like shown here.
-#
-# import os
-# import sys
-# sys.path.insert(0, os.path.abspath('.'))
+
+import os
+import sys
+sys.path.insert(0, os.path.abspath('.'))
 
 
 # -- Project information -----------------------------------------------------
@@ -21,6 +21,16 @@
 copyright = '2020 - 2023, Alt-Ergo developers'
 author = 'Alt-Ergo developers'
 
+# -- Custom lexer ------------------------------------------------------------
+
+# Import our custom lexer
+from alt_ergo_lexer import AltErgoLexer
+from sphinx.highlighting import lexers
+lexers['alt-ergo'] = AltErgoLexer()
+
+# Use alt-ergo as the default language
+highlight_language = 'alt-ergo'
+
 # -- Entry point -------------------------------------------------------------
 
 master_doc = 'index'
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index c8d65dbb00..69640f02e3 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -574,7 +574,7 @@ module Main_Default : S = struct
     {t with terms = Expr.Set.union t.terms choices_terms}, choices_terms
 
   let do_case_split t origin =
-    if Options.get_case_split_policy () == origin then
+    if false && Options.get_case_split_policy () == origin then
       do_case_split_aux t ~for_model:false
     else
       t, SE.empty