diff --git a/NEWS b/NEWS
index 5e197289e..587a69c48 100644
--- a/NEWS
+++ b/NEWS
@@ -20,6 +20,10 @@ New in spot 2.7.2.dev (not yet released)
     'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1
     state instead of 4.)
 
+  - acc_cond::acc_code::top_disjuncts() and
+    acc_cond::acc_code::top_conjuncts() can be used to split an
+    acceptance condition on the top-level & or |.
+
   Bugs fixed:
 
   - When processing CSV files with MSDOS-style \r\n line endings,
diff --git a/python/spot/impl.i b/python/spot/impl.i
index c8b86a160..8cad8aaf9 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -473,6 +473,7 @@ namespace std {
   %template(vectorformula) vector<spot::formula>;
   %template(vectorunsigned) vector<unsigned>;
   %template(vectorpairunsigned) vector<pair<unsigned, unsigned>>;
+  %template(vectoracccode) vector<spot::acc_cond::acc_code>;
   %template(vectorbool) vector<bool>;
   %template(vectorbdd) vector<bdd>;
   %template(vectorstring) vector<string>;
diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index d336a948e..2d9f71309 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -1232,6 +1232,74 @@ namespace spot
     return rescode;
   }
 
+  namespace
+  {
+    static std::vector<acc_cond::acc_code>
+    top_clauses(const acc_cond::acc_code& code,
+                acc_cond::acc_op connect, acc_cond::acc_op inf_fin)
+    {
+      std::vector<acc_cond::acc_code> res;
+
+      if (!code.empty())
+        {
+          auto pos = &code.back();
+          auto start = &code.front();
+          assert(pos - pos->sub.size == start);
+          if (pos->sub.op == connect)
+            {
+              do
+                {
+                  --pos;
+                  if (pos->sub.op == inf_fin)
+                    {
+                      for (unsigned d: pos[-1].mark.sets())
+                        {
+                          acc_cond::acc_code tmp;
+                          tmp.resize(2);
+                          tmp[0].mark = {d};
+                          tmp[1].sub.op = inf_fin;
+                          tmp[1].sub.size = 1;
+                          res.emplace_back(tmp);
+                        }
+                    }
+                  else
+                    {
+                      res.emplace_back(pos);
+                    }
+                  pos -= pos->sub.size;
+                }
+              while (pos > start);
+              return res;
+            }
+          if (pos->sub.op == inf_fin)
+            {
+              for (unsigned d: pos[-1].mark.sets())
+                {
+                  acc_cond::acc_code tmp;
+                  tmp.resize(2);
+                  tmp[0].mark = {d};
+                  tmp[1].sub.op = inf_fin;
+                  tmp[1].sub.size = 1;
+                  res.emplace_back(tmp);
+                }
+              return res;
+            }
+        }
+      res.emplace_back(code);
+      return res;
+    }
+  }
+
+  std::vector<acc_cond::acc_code> acc_cond::acc_code::top_disjuncts() const
+  {
+    return top_clauses(*this, acc_cond::acc_op::Or, acc_cond::acc_op::Fin);
+  }
+
+  std::vector<acc_cond::acc_code> acc_cond::acc_code::top_conjuncts() const
+  {
+    return top_clauses(*this, acc_cond::acc_op::And, acc_cond::acc_op::Inf);
+  }
+
   std::pair<bool, acc_cond::mark_t>
   acc_cond::sat_unsat_mark(bool sat) const
   {
diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index 74cd94411..3a7f2db6f 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2019 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -1120,6 +1120,27 @@ namespace spot
       /// This implementation is the dual of `to_dnf()`.
       acc_code to_cnf() const;
 
+
+      /// \brief Return the top-level disjuncts.
+      ///
+      /// For instance, if the formula is
+      /// Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns
+      /// [Fin(0), Fin(1), Fin(2)&(Inf(3)|Fin(4))].
+      ///
+      /// If the formula is not a disjunction, this returns
+      /// a vector with the formula as only element.
+      std::vector<acc_code> top_disjuncts() const;
+
+      /// \brief Return the top-level conjuncts.
+      ///
+      /// For instance, if the formula is
+      /// Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4))), this returns
+      /// [Fin(0), Fin(1), Fin(2)&(Inf(3)|Fin(4))].
+      ///
+      /// If the formula is not a conjunction, this returns
+      /// a vector with the formula as only element.
+      std::vector<acc_code> top_conjuncts() const;
+
       /// \brief Complement an acceptance formula.
       ///
       /// Also known as "dualizing the acceptance condition" since
diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb
index 852a21510..c406ebdc3 100644
--- a/tests/python/acc_cond.ipynb
+++ b/tests/python/acc_cond.ipynb
@@ -821,14 +821,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "# `acc_cond`\n",
-    "\n",
-    "Automata store their acceptance condition as an instance of the `acc_cond` class.\n",
-    "This class can be thought of as a pair `(n, code)`, where `n` is an integer that tells how many acceptance sets are used, while the `code` is an instance of `acc_code` and encodes the formula over *a subset* of these acceptance sets.  We usually have `n == code.used_sets().max_set())`, but `n` can be larger.\n",
-    "\n",
-    "It is OK if an automaton declares that is uses 3 sets, even if the acceptance condition formula only uses set number 1.  The extra two sets will have no impact on the language, even if they are used in the automaton.\n",
-    "\n",
-    "The `acc_cond` objects are usually not created by hand: automata have dedicated methods for that.  But for the purpose of this notebook, let's do it:"
+    "If the top-level operators is a conjunct or disjunct, the following methods returns lists of clauses."
    ]
   },
   {
@@ -837,26 +830,40 @@
    "metadata": {},
    "outputs": [
     {
-     "data": {
-      "text/plain": [
-       "spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
-      ]
-     },
-     "execution_count": 33,
-     "metadata": {},
-     "output_type": "execute_result"
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "spot.acc_code(\"(Fin(0)|Fin(3)) | (Inf(1) & Fin(2))\")\n",
+      "(spot.acc_code(\"Fin(0)\"), spot.acc_code(\"Fin(3)\"), spot.acc_code(\"Inf(1) & Fin(2)\"))\n",
+      "spot.acc_code(\"(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))\")\n",
+      "(spot.acc_code(\"Inf(0)\"), spot.acc_code(\"Inf(1)\"), spot.acc_code(\"Fin(2)|Fin(3)\"))\n",
+      "(spot.acc_code(\"(Inf(0)&Inf(1)) & (Fin(2)|Fin(3))\"),)\n"
+     ]
     }
    ],
    "source": [
-    "acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n",
-    "acc"
+    "c = spot.acc_code('Fin(0)|(Inf(1)&Fin(2))|Fin(3)')\n",
+    "print(repr(c))\n",
+    "print(c.top_disjuncts())\n",
+    "c = spot.acc_code('Inf(0)&Inf(1)&(Fin(2)|Fin(3))')\n",
+    "print(repr(c))\n",
+    "print(c.top_conjuncts())\n",
+    "# Nothing to split here as the top operator is not a disjunction\n",
+    "print(c.top_disjuncts())"
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "For convenience, you can pass the string directly:"
+    "# `acc_cond`\n",
+    "\n",
+    "Automata store their acceptance condition as an instance of the `acc_cond` class.\n",
+    "This class can be thought of as a pair `(n, code)`, where `n` is an integer that tells how many acceptance sets are used, while the `code` is an instance of `acc_code` and encodes the formula over *a subset* of these acceptance sets.  We usually have `n == code.used_sets().max_set())`, but `n` can be larger.\n",
+    "\n",
+    "It is OK if an automaton declares that is uses 3 sets, even if the acceptance condition formula only uses set number 1.  The extra two sets will have no impact on the language, even if they are used in the automaton.\n",
+    "\n",
+    "The `acc_cond` objects are usually not created by hand: automata have dedicated methods for that.  But for the purpose of this notebook, let's do it:"
    ]
   },
   {
@@ -876,10 +883,17 @@
     }
    ],
    "source": [
-    "acc = spot.acc_cond(4, 'Rabin 2')\n",
+    "acc = spot.acc_cond(4, spot.acc_code('Rabin 2'))\n",
     "acc"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "For convenience, you can pass the string directly:"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": 35,
@@ -888,7 +902,7 @@
     {
      "data": {
       "text/plain": [
-       "4"
+       "spot.acc_cond(4, \"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
       ]
      },
      "execution_count": 35,
@@ -897,7 +911,8 @@
     }
    ],
    "source": [
-    "acc.num_sets()"
+    "acc = spot.acc_cond(4, 'Rabin 2')\n",
+    "acc"
    ]
   },
   {
@@ -908,7 +923,7 @@
     {
      "data": {
       "text/plain": [
-       "spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
+       "4"
       ]
      },
      "execution_count": 36,
@@ -916,6 +931,26 @@
      "output_type": "execute_result"
     }
    ],
+   "source": [
+    "acc.num_sets()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 37,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "spot.acc_code(\"(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))\")"
+      ]
+     },
+     "execution_count": 37,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "acc.get_acceptance()"
    ]
@@ -929,7 +964,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 37,
+   "execution_count": 38,
    "metadata": {},
    "outputs": [
     {
@@ -938,7 +973,7 @@
        "spot.acc_cond(4, \"t\")"
       ]
      },
-     "execution_count": 37,
+     "execution_count": 38,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -950,7 +985,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 38,
+   "execution_count": 39,
    "metadata": {},
    "outputs": [
     {
@@ -959,7 +994,7 @@
        "spot.acc_cond(6, \"t\")"
       ]
      },
-     "execution_count": 38,
+     "execution_count": 39,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -971,7 +1006,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 39,
+   "execution_count": 40,
    "metadata": {},
    "outputs": [
     {
@@ -980,7 +1015,7 @@
        "spot.acc_cond(6, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
       ]
      },
-     "execution_count": 39,
+     "execution_count": 40,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -997,34 +1032,6 @@
     "Calling the constructor of `acc_cond` by passing just an instance of `acc_code` (or a string that will be passed to the `acc_code` constructor) will automatically set the number of acceptance sets to the minimum needed by the formula:"
    ]
   },
-  {
-   "cell_type": "code",
-   "execution_count": 40,
-   "metadata": {},
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
-      ]
-     },
-     "execution_count": 40,
-     "metadata": {},
-     "output_type": "execute_result"
-    }
-   ],
-   "source": [
-    "acc = spot.acc_cond('Streett 2')\n",
-    "acc"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "metadata": {},
-   "source": [
-    "The above is in fact just syntactic sugar for:"
-   ]
-  },
   {
    "cell_type": "code",
    "execution_count": 41,
@@ -1041,6 +1048,34 @@
      "output_type": "execute_result"
     }
    ],
+   "source": [
+    "acc = spot.acc_cond('Streett 2')\n",
+    "acc"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "The above is in fact just syntactic sugar for:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 42,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\")"
+      ]
+     },
+     "execution_count": 42,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     "code = spot.acc_code('Streett 2')\n",
     "acc = spot.acc_cond(code.used_sets().max_set(), code)\n",
@@ -1056,7 +1091,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 42,
+   "execution_count": 43,
    "metadata": {},
    "outputs": [
     {
@@ -1065,7 +1100,7 @@
        "spot.acc_cond(4, \"Inf(0)&Inf(1)&Inf(2)&Inf(3)\")"
       ]
      },
-     "execution_count": 42,
+     "execution_count": 43,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1085,7 +1120,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 43,
+   "execution_count": 44,
    "metadata": {},
    "outputs": [
     {
@@ -1118,7 +1153,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 44,
+   "execution_count": 45,
    "metadata": {},
    "outputs": [
     {
@@ -1147,7 +1182,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 45,
+   "execution_count": 46,
    "metadata": {},
    "outputs": [
     {
@@ -1179,7 +1214,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 46,
+   "execution_count": 47,
    "metadata": {},
    "outputs": [
     {
@@ -1209,7 +1244,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 47,
+   "execution_count": 48,
    "metadata": {},
    "outputs": [
     {
@@ -1234,7 +1269,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 48,
+   "execution_count": 49,
    "metadata": {},
    "outputs": [
     {
@@ -1243,7 +1278,7 @@
        "spot.mark_t([0, 1, 2, 3])"
       ]
      },
-     "execution_count": 48,
+     "execution_count": 49,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -1262,7 +1297,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 49,
+   "execution_count": 50,
    "metadata": {},
    "outputs": [
     {
@@ -1292,7 +1327,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 50,
+   "execution_count": 51,
    "metadata": {},
    "outputs": [
     {
@@ -1311,7 +1346,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 51,
+   "execution_count": 52,
    "metadata": {},
    "outputs": [
     {
@@ -1331,7 +1366,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 52,
+   "execution_count": 53,
    "metadata": {},
    "outputs": [
     {
@@ -1366,7 +1401,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.6.7"
+   "version": "3.7.3rc1"
   }
  },
  "nbformat": 4,