diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb
index 47b908c75..20e96c17d 100644
--- a/tests/python/formulas.ipynb
+++ b/tests/python/formulas.ipynb
@@ -10,7 +10,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 1,
+   "execution_count": 10,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -27,7 +27,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 2,
+   "execution_count": 11,
    "metadata": {},
    "outputs": [
     {
@@ -39,7 +39,7 @@
        "spot.formula(\"p1 U (p2 R (p3 & !p4))\")"
       ]
      },
-     "execution_count": 2,
+     "execution_count": 11,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -51,7 +51,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 3,
+   "execution_count": 12,
    "metadata": {},
    "outputs": [
     {
@@ -63,7 +63,7 @@
        "spot.formula(\"{a;first_match({b[*];c[+]}[:*3..5];b)}<>-> (c & GFb)\")"
       ]
      },
-     "execution_count": 3,
+     "execution_count": 12,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -81,7 +81,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 4,
+   "execution_count": 13,
    "metadata": {},
    "outputs": [
     {
@@ -93,7 +93,7 @@
        "spot.formula(\"c & (a | b)\")"
       ]
      },
-     "execution_count": 4,
+     "execution_count": 13,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -111,7 +111,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 14,
    "metadata": {},
    "outputs": [
     {
@@ -123,7 +123,7 @@
        "spot.formula(\"c & (a | b)\")"
       ]
      },
-     "execution_count": 5,
+     "execution_count": 14,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -142,7 +142,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 15,
    "metadata": {},
    "outputs": [
     {
@@ -151,7 +151,7 @@
        "'p1 U (p2 R (p3 & !p4))'"
       ]
      },
-     "execution_count": 6,
+     "execution_count": 15,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -169,7 +169,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 16,
    "metadata": {},
    "outputs": [
     {
@@ -201,7 +201,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 17,
    "metadata": {},
    "outputs": [
     {
@@ -231,64 +231,63 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "The specifiers that can be used with `format` are documented as follows:"
+    "The specifiers that can be used with `format` are documented as follows.\n",
+    "(Note: As this document is part of our test-suite we have to use `print(x.__doc__)` instead of `help(x)` to work around some formating changes introduced in Python 3.12's `help()`.)"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 18,
    "metadata": {},
    "outputs": [
     {
      "name": "stdout",
      "output_type": "stream",
      "text": [
-      "Help on function __format__ in module spot:\n",
+      "Format the formula according to `spec`.\n",
       "\n",
-      "__format__(self, spec)\n",
-      "    Format the formula according to `spec`.\n",
-      "    \n",
-      "    Parameters\n",
-      "    ----------\n",
-      "    spec : str, optional\n",
-      "        a list of letters that specify how the formula\n",
-      "        should be formatted.\n",
-      "    \n",
-      "    Supported specifiers\n",
-      "    --------------------\n",
-      "    \n",
-      "    - 'f': use Spot's syntax (default)\n",
-      "    - '8': use Spot's syntax in UTF-8 mode\n",
-      "    - 's': use Spin's syntax\n",
-      "    - 'l': use LBT's syntax\n",
-      "    - 'w': use Wring's syntax\n",
-      "    - 'x': use LaTeX output\n",
-      "    - 'X': use self-contained LaTeX output\n",
-      "    - 'j': use self-contained LaTeX output, adjusted for MathJax\n",
-      "    \n",
-      "    Add some of those letters for additional options:\n",
-      "    \n",
-      "    - 'p': use full parentheses\n",
-      "    - 'c': escape the formula for CSV output (this will\n",
-      "           enclose the formula in double quotes, and escape\n",
-      "           any included double quotes)\n",
-      "    - 'h': escape the formula for HTML output\n",
-      "    - 'd': escape double quotes and backslash,\n",
-      "           for use in C-strings (the outermost double\n",
-      "           quotes are *not* added)\n",
-      "    - 'q': quote and escape for shell output, using single\n",
-      "           quotes or double quotes depending on the contents.\n",
-      "    - '[...]': rewrite away all the operators specified in brackets,\n",
-      "           using spot.unabbreviate().\n",
-      "    \n",
-      "    - ':spec': pass the remaining specification to the\n",
-      "               formating function for strings.\n",
-      "\n"
+      "        Parameters\n",
+      "        ----------\n",
+      "        spec : str, optional\n",
+      "            a list of letters that specify how the formula\n",
+      "            should be formatted.\n",
+      "\n",
+      "        Supported specifiers\n",
+      "        --------------------\n",
+      "\n",
+      "        - 'f': use Spot's syntax (default)\n",
+      "        - '8': use Spot's syntax in UTF-8 mode\n",
+      "        - 's': use Spin's syntax\n",
+      "        - 'l': use LBT's syntax\n",
+      "        - 'w': use Wring's syntax\n",
+      "        - 'x': use LaTeX output\n",
+      "        - 'X': use self-contained LaTeX output\n",
+      "        - 'j': use self-contained LaTeX output, adjusted for MathJax\n",
+      "\n",
+      "        Add some of those letters for additional options:\n",
+      "\n",
+      "        - 'p': use full parentheses\n",
+      "        - 'c': escape the formula for CSV output (this will\n",
+      "               enclose the formula in double quotes, and escape\n",
+      "               any included double quotes)\n",
+      "        - 'h': escape the formula for HTML output\n",
+      "        - 'd': escape double quotes and backslash,\n",
+      "               for use in C-strings (the outermost double\n",
+      "               quotes are *not* added)\n",
+      "        - 'q': quote and escape for shell output, using single\n",
+      "               quotes or double quotes depending on the contents.\n",
+      "        - '[...]': rewrite away all the operators specified in brackets,\n",
+      "               using spot.unabbreviate().\n",
+      "\n",
+      "        - ':spec': pass the remaining specification to the\n",
+      "                   formating function for strings.\n",
+      "\n",
+      "        \n"
      ]
     }
    ],
    "source": [
-    "help(spot.formula.__format__)"
+    "print(spot.formula.__format__.__doc__)"
    ]
   },
   {
@@ -300,7 +299,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 10,
+   "execution_count": 19,
    "metadata": {},
    "outputs": [
     {
@@ -309,7 +308,7 @@
        "True"
       ]
      },
-     "execution_count": 10,
+     "execution_count": 19,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -320,7 +319,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 20,
    "metadata": {},
    "outputs": [
     {
@@ -329,7 +328,7 @@
        "False"
       ]
      },
-     "execution_count": 11,
+     "execution_count": 20,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -347,7 +346,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 21,
    "metadata": {},
    "outputs": [
     {
@@ -356,7 +355,7 @@
        "True"
       ]
      },
-     "execution_count": 12,
+     "execution_count": 21,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -367,7 +366,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 22,
    "metadata": {},
    "outputs": [
     {
@@ -376,7 +375,7 @@
        "False"
       ]
      },
-     "execution_count": 13,
+     "execution_count": 22,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -387,7 +386,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 23,
    "metadata": {},
    "outputs": [
     {
@@ -396,7 +395,7 @@
        "True"
       ]
      },
-     "execution_count": 14,
+     "execution_count": 23,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -414,7 +413,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 24,
    "metadata": {},
    "outputs": [
     {
@@ -426,7 +425,7 @@
        "spot.formula(\"\\\"a > b\\\" & \\\"proc[2]@init\\\" & GF_foo_\")"
       ]
      },
-     "execution_count": 15,
+     "execution_count": 24,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -437,7 +436,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 25,
    "metadata": {},
    "outputs": [
     {
@@ -449,7 +448,7 @@
        "spot.formula(\"a & b & GFc\")"
       ]
      },
-     "execution_count": 16,
+     "execution_count": 25,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -460,7 +459,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 26,
    "metadata": {},
    "outputs": [
     {
@@ -472,7 +471,7 @@
        "spot.formula(\"p0 & p1 & GFp2\")"
       ]
      },
-     "execution_count": 17,
+     "execution_count": 26,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -490,7 +489,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 27,
    "metadata": {},
    "outputs": [
     {
@@ -711,7 +710,7 @@
        "<spot.jupyter.SVG object>"
       ]
      },
-     "execution_count": 18,
+     "execution_count": 27,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -729,7 +728,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 19,
+   "execution_count": 28,
    "metadata": {},
    "outputs": [
     {
@@ -765,7 +764,7 @@
        "<spot.jupyter.SVG object>"
       ]
      },
-     "execution_count": 19,
+     "execution_count": 28,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -776,7 +775,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 29,
    "metadata": {},
    "outputs": [
     {
@@ -785,7 +784,7 @@
        "'recurrence'"
       ]
      },
-     "execution_count": 20,
+     "execution_count": 29,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -796,7 +795,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 30,
    "metadata": {},
    "outputs": [
     {
@@ -808,7 +807,7 @@
        "spot.formula(\"F(a & X(!a & b))\")"
       ]
      },
-     "execution_count": 21,
+     "execution_count": 30,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -826,7 +825,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": 31,
    "metadata": {},
    "outputs": [
     {
@@ -838,7 +837,7 @@
        "spot.formula(\"F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b))) | (!a & b & (G!a | Ga) & (G!b | Gb))))\")"
       ]
      },
-     "execution_count": 22,
+     "execution_count": 31,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -856,7 +855,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 23,
+   "execution_count": 32,
    "metadata": {},
    "outputs": [
     {
@@ -868,7 +867,7 @@
        "spot.formula(\"(0 R !(a <-> b)) -> (1 U (a <-> b))\")"
       ]
      },
-     "execution_count": 23,
+     "execution_count": 32,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -880,7 +879,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": 33,
    "metadata": {},
    "outputs": [
     {
@@ -892,7 +891,7 @@
        "spot.formula(\"(1 U ((a & b) | (!a & !b))) | !(0 R ((!a & b) | (a & !b)))\")"
       ]
      },
-     "execution_count": 24,
+     "execution_count": 33,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -910,7 +909,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": 34,
    "metadata": {},
    "outputs": [
     {
@@ -946,7 +945,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 26,
+   "execution_count": 35,
    "metadata": {},
    "outputs": [
     {
@@ -986,7 +985,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 27,
+   "execution_count": 36,
    "metadata": {},
    "outputs": [
     {