diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc
index e3c3bb6c5..af255a167 100644
--- a/spot/twaalgos/aiger.cc
+++ b/spot/twaalgos/aiger.cc
@@ -637,19 +637,44 @@ namespace spot
     // De-morgan
     // !(!v&low | v&high) = !(!v&low) & !(v&high)
     // !v&low | v&high = !(!(!v&low) & !(v&high))
+    // note that if low or high are T
+    // we can simplify the formula
+    // given that low / high is T
+    // then !(!v&low) & !(v&high) can be simplified to
+    // !v&low | v&high = !v | high / low | v
+    // = !(v & !high) /  !(!low & !v)
+    // The case when low / high is ⊥ is automatically treated
     auto b_it = bdd2var_.find(b.id());
     if (b_it != bdd2var_.end())
       return b_it->second;
 
-    // todo
-//    unsigned v_var = bdd2var_.at(bdd_var(b));
     unsigned v_var = bdd2var_.at(bdd_ithvar(bdd_var(b)).id());
 
     unsigned b_branch_var[2] = {bdd2INFvar(bdd_low(b)),
                                 bdd2INFvar(bdd_high(b))};
 
-    unsigned r = aig_not(aig_and(v_var, b_branch_var[1]));
-    unsigned l = aig_not(aig_and(aig_not(v_var), b_branch_var[0]));
+    unsigned l;
+    unsigned r;
+
+    if (b_branch_var[0] == aig_true())
+      {
+        // low == T
+        l = v_var;
+        r = aig_not(b_branch_var[1]);
+      }
+    else if (b_branch_var[1] == aig_true())
+      {
+        // high == T
+        l = aig_not(b_branch_var[0]);
+        r = aig_not(v_var);
+      }
+    else
+      {
+        // General case
+        r = aig_not(aig_and(v_var, b_branch_var[1]));
+        l = aig_not(aig_and(aig_not(v_var), b_branch_var[0]));
+      }
+
     return aig_not(aig_and(l, r));
   }
 
diff --git a/tests/python/_synthesis.ipynb b/tests/python/_synthesis.ipynb
index 6952eadd3..4c203a86e 100644
--- a/tests/python/_synthesis.ipynb
+++ b/tests/python/_synthesis.ipynb
@@ -738,7 +738,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc883a7720> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc33a0f0> >"
       ]
      },
      "execution_count": 8,
@@ -821,7 +821,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc883a7720> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc33a0f0> >"
       ]
      },
      "execution_count": 9,
@@ -945,7 +945,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc8833aa80> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc345660> >"
       ]
      },
      "execution_count": 10,
@@ -1043,7 +1043,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c2ab0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc3486c0> >"
       ]
      },
      "execution_count": 11,
@@ -1211,7 +1211,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc8833ae70> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc345ae0> >"
       ]
      },
      "execution_count": 12,
@@ -1420,7 +1420,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c2240> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc345e40> >"
       ]
      },
      "execution_count": 13,
@@ -1578,7 +1578,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880bdc30> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc364a20> >"
       ]
      },
      "execution_count": 14,
@@ -1722,7 +1722,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880bdc30> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc364a20> >"
       ]
      },
      "execution_count": 15,
@@ -1869,7 +1869,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c5210> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc35a2d0> >"
       ]
      },
      "execution_count": 16,
@@ -2014,7 +2014,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c5210> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc35a2d0> >"
       ]
      },
      "execution_count": 17,
@@ -2561,7 +2561,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c5d50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc35af00> >"
       ]
      },
      "execution_count": 18,
@@ -2715,7 +2715,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c5d50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc35af00> >"
       ]
      },
      "execution_count": 19,
@@ -2873,7 +2873,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880cd090> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc36d240> >"
       ]
      },
      "metadata": {},
@@ -4215,7 +4215,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880bdc00> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc3910f0> >"
       ]
      },
      "execution_count": 20,
@@ -4698,7 +4698,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880bdc00> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc3910f0> >"
       ]
      },
      "execution_count": 21,
@@ -4831,7 +4831,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880cd2a0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc364570> >"
       ]
      },
      "metadata": {},
@@ -5509,7 +5509,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c55a0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc35a9c0> >"
       ]
      },
      "execution_count": 22,
@@ -5748,7 +5748,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c55a0> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc35a9c0> >"
       ]
      },
      "execution_count": 23,
@@ -5838,7 +5838,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c5a50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc3646c0> >"
       ]
      },
      "metadata": {},
@@ -5932,7 +5932,7 @@
        "</svg>\n"
       ],
       "text/plain": [
-       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fcc880c5a50> >"
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc3646c0> >"
       ]
      },
      "metadata": {},
@@ -5955,10 +5955,414 @@
     "display(aut)"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "7efe7450",
+   "metadata": {},
+   "source": [
+    "# Test improved aiger INF encoding"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 25,
+   "id": "31872ccc",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"349pt\" height=\"136pt\"\n",
+       " viewBox=\"0.00 0.00 349.00 136.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 132)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-132 345,-132 345,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"167.5\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"159.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;1 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-45C2.79,-45 17.15,-45 30.63,-45\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-45 30.94,-48.15 34.44,-45 30.94,-45 30.94,-45 30.94,-45 34.44,-45 30.94,-41.85 37.94,-45 37.94,-45\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"233,-90 206,-72 233,-54 260,-72 233,-90\"/>\n",
+       "<text text-anchor=\"middle\" x=\"233\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.1,-47.64C104.25,-52.29 167.16,-62 203.82,-67.65\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"210.78,-68.73 203.38,-70.77 207.32,-68.19 203.86,-67.66 203.86,-67.66 203.86,-67.66 207.32,-68.19 204.34,-64.55 210.78,-68.73 210.78,-68.73\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-67.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b &amp; !c &amp; !d</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"233,-36 206,-18 233,0 260,-18 233,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"233\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;3 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M72.71,-37.59C78.64,-35.1 85.51,-32.56 92,-31 127.83,-22.36 170.11,-19.39 198.75,-18.41\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"206.09,-18.19 199.19,-21.55 202.59,-18.29 199.09,-18.4 199.09,-18.4 199.09,-18.4 202.59,-18.29 199,-15.25 206.09,-18.19 206.09,-18.19\"/>\n",
+       "<text text-anchor=\"start\" x=\"108.5\" y=\"-34.8\" font-family=\"Lato\" font-size=\"14.00\">a | b | c | d</text>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"323\" cy=\"-56\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"323\" y=\"-52.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M304.75,-55.18C296.58,-55.1 286.73,-55.45 278,-57 271,-58.24 263.6,-60.41 256.91,-62.71\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"249.99,-65.23 255.49,-59.88 253.28,-64.03 256.56,-62.84 256.56,-62.84 256.56,-62.84 253.28,-64.03 257.64,-65.8 249.99,-65.23 249.99,-65.23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"282.5\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;0 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M256.92,-74.12C266.34,-74.44 277.29,-74.11 287,-72 291.46,-71.03 296.02,-69.44 300.33,-67.63\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"306.82,-64.66 301.76,-70.44 303.63,-66.12 300.45,-67.57 300.45,-67.57 300.45,-67.57 303.63,-66.12 299.14,-64.71 306.82,-64.66 306.82,-64.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"282.5\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;0 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>3&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M252.48,-23.32C262.82,-26.53 275.84,-30.97 287,-36 291.63,-38.09 296.45,-40.6 300.97,-43.12\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"307.34,-46.79 299.7,-46.03 304.31,-45.04 301.27,-43.3 301.27,-43.3 301.27,-43.3 304.31,-45.04 302.85,-40.57 307.34,-46.79 307.34,-46.79\"/>\n",
+       "<text text-anchor=\"start\" x=\"279\" y=\"-39.8\" font-family=\"Lato\" font-size=\"14.00\">x</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbccc3911e0> >"
+      ]
+     },
+     "execution_count": 25,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "si = spot.synthesis_info()\n",
+    "\n",
+    "aut = spot.ltl_to_game(\"(a|b|c|d)->x\", [\"x\"], si)\n",
+    "aut"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "id": "9064bc60",
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "True\n"
+     ]
+    }
+   ],
+   "source": [
+    "print(spot.solve_game(aut))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 27,
+   "id": "303ada1e",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"349pt\" height=\"136pt\"\n",
+       " viewBox=\"0.00 0.00 349.00 136.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 132)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-132 345,-132 345,4 -4,4\"/>\n",
+       "<text text-anchor=\"start\" x=\"167.5\" y=\"-112.8\" font-family=\"Lato\" font-size=\"14.00\">t</text>\n",
+       "<text text-anchor=\"start\" x=\"159.5\" y=\"-97.8\" font-family=\"Lato\" font-size=\"14.00\">[all]</text>\n",
+       "<!-- I -->\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-45\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"56\" y=\"-41.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+       "</g>\n",
+       "<!-- I&#45;&gt;0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>I&#45;&gt;0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M1.15,-45C2.79,-45 17.15,-45 30.63,-45\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"37.94,-45 30.94,-48.15 34.44,-45 30.94,-45 30.94,-45 30.94,-45 34.44,-45 30.94,-41.85 37.94,-45 37.94,-45\"/>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"233,-90 206,-72 233,-54 260,-72 233,-90\"/>\n",
+       "<text text-anchor=\"middle\" x=\"233\" y=\"-68.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;2 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M74.1,-47.64C104.25,-52.29 167.16,-62 203.82,-67.65\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"210.78,-68.73 203.38,-70.77 207.32,-68.19 203.86,-67.66 203.86,-67.66 203.86,-67.66 207.32,-68.19 204.34,-64.55 210.78,-68.73 210.78,-68.73\"/>\n",
+       "<text text-anchor=\"start\" x=\"92\" y=\"-67.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b &amp; !c &amp; !d</text>\n",
+       "</g>\n",
+       "<!-- 3 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>3</title>\n",
+       "<polygon fill=\"#ffffaa\" stroke=\"black\" points=\"233,-36 206,-18 233,0 260,-18 233,-36\"/>\n",
+       "<text text-anchor=\"middle\" x=\"233\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;3 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>0&#45;&gt;3</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M72.77,-38.17C78.69,-35.86 85.56,-33.49 92,-32 128.15,-23.62 170.7,-20.26 199.32,-18.91\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"206.65,-18.59 199.79,-22.04 203.15,-18.74 199.65,-18.89 199.65,-18.89 199.65,-18.89 203.15,-18.74 199.52,-15.75 206.65,-18.59 206.65,-18.59\"/>\n",
+       "<text text-anchor=\"start\" x=\"108.5\" y=\"-35.8\" font-family=\"Lato\" font-size=\"14.00\">a | b | c | d</text>\n",
+       "</g>\n",
+       "<!-- 1 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>1</title>\n",
+       "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"323\" cy=\"-56\" rx=\"18\" ry=\"18\"/>\n",
+       "<text text-anchor=\"middle\" x=\"323\" y=\"-52.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;1 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>2&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M256.92,-74.12C266.34,-74.44 277.29,-74.11 287,-72 291.46,-71.03 296.02,-69.44 300.33,-67.63\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"306.82,-64.66 301.76,-70.44 303.63,-66.12 300.45,-67.57 300.45,-67.57 300.45,-67.57 303.63,-66.12 299.14,-64.71 306.82,-64.66 306.82,-64.66\"/>\n",
+       "<text text-anchor=\"middle\" x=\"282.5\" y=\"-76.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "<!-- 3&#45;&gt;1 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>3&#45;&gt;1</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M251.93,-23.67C262.33,-27.14 275.58,-31.89 287,-37 291.49,-39.01 296.2,-41.37 300.64,-43.74\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"306.92,-47.16 299.27,-46.57 303.85,-45.48 300.78,-43.81 300.78,-43.81 300.78,-43.81 303.85,-45.48 302.28,-41.04 306.92,-47.16 306.92,-47.16\"/>\n",
+       "<text text-anchor=\"start\" x=\"279\" y=\"-40.8\" font-family=\"Lato\" font-size=\"14.00\">x</text>\n",
+       "</g>\n",
+       "<!-- 1&#45;&gt;2 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>1&#45;&gt;2</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M304.75,-55.18C296.58,-55.1 286.73,-55.45 278,-57 271,-58.24 263.6,-60.41 256.91,-62.71\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"249.99,-65.23 255.49,-59.88 253.28,-64.03 256.56,-62.84 256.56,-62.84 256.56,-62.84 253.28,-64.03 257.64,-65.8 249.99,-65.23 249.99,-65.23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"282.5\" y=\"-60.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fbcd407ca20> >"
+      ]
+     },
+     "execution_count": 27,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "ctrl = spot.solved_game_to_split_mealy(aut)\n",
+    "ctrl"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "id": "9874a530",
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "image/svg+xml": [
+       "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
+       "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
+       " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
+       "<!-- Generated by graphviz version 2.43.0 (0)\n",
+       " -->\n",
+       "<!-- Pages: 1 -->\n",
+       "<svg width=\"397pt\" height=\"462pt\"\n",
+       " viewBox=\"0.00 0.00 396.70 461.98\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<g id=\"graph0\" class=\"graph\" transform=\"scale(1.0 1.0) rotate(0) translate(4 457.98)\">\n",
+       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-457.98 392.7,-457.98 392.7,4 -4,4\"/>\n",
+       "<!-- 10 -->\n",
+       "<g id=\"node1\" class=\"node\">\n",
+       "<title>10</title>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"91.7,-122.75 26.7,-122.75 26.7,-86.75 91.7,-86.75 91.7,-122.75\"/>\n",
+       "<text text-anchor=\"middle\" x=\"59.2\" y=\"-101.05\" font-family=\"Times,serif\" font-size=\"14.00\">L0_out</text>\n",
+       "</g>\n",
+       "<!-- 18 -->\n",
+       "<g id=\"node5\" class=\"node\">\n",
+       "<title>18</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"95.2\" cy=\"-349.24\" rx=\"23\" ry=\"23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"95.2\" y=\"-345.54\" font-family=\"Times,serif\" font-size=\"14.00\">18</text>\n",
+       "</g>\n",
+       "<!-- 10&#45;&gt;18 -->\n",
+       "<g id=\"edge9\" class=\"edge\">\n",
+       "<title>10&#45;&gt;18</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M61.73,-122.8C67.78,-163.54 83.13,-266.98 90.76,-318.35\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"91.37\" cy=\"-322.47\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 12 -->\n",
+       "<g id=\"node2\" class=\"node\">\n",
+       "<title>12</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"132.2\" cy=\"-104.75\" rx=\"23\" ry=\"23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"132.2\" y=\"-101.05\" font-family=\"Times,serif\" font-size=\"14.00\">12</text>\n",
+       "</g>\n",
+       "<!-- 14 -->\n",
+       "<g id=\"node3\" class=\"node\">\n",
+       "<title>14</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"166.2\" cy=\"-186.24\" rx=\"23\" ry=\"23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"166.2\" y=\"-182.54\" font-family=\"Times,serif\" font-size=\"14.00\">14</text>\n",
+       "</g>\n",
+       "<!-- 12&#45;&gt;14 -->\n",
+       "<g id=\"edge5\" class=\"edge\">\n",
+       "<title>12&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M140.95,-126.22C144.79,-135.19 149.37,-145.89 153.56,-155.7\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"150.44,-157.3 157.59,-165.12 156.87,-154.55 150.44,-157.3\"/>\n",
+       "</g>\n",
+       "<!-- 16 -->\n",
+       "<g id=\"node4\" class=\"node\">\n",
+       "<title>16</title>\n",
+       "<ellipse fill=\"none\" stroke=\"black\" cx=\"166.2\" cy=\"-267.74\" rx=\"23\" ry=\"23\"/>\n",
+       "<text text-anchor=\"middle\" x=\"166.2\" y=\"-264.04\" font-family=\"Times,serif\" font-size=\"14.00\">16</text>\n",
+       "</g>\n",
+       "<!-- 14&#45;&gt;16 -->\n",
+       "<g id=\"edge7\" class=\"edge\">\n",
+       "<title>14&#45;&gt;16</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M166.2,-209.39C166.2,-217.29 166.2,-226.36 166.2,-234.92\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"162.7,-234.99 166.2,-244.99 169.7,-234.99 162.7,-234.99\"/>\n",
+       "</g>\n",
+       "<!-- 16&#45;&gt;18 -->\n",
+       "<g id=\"edge10\" class=\"edge\">\n",
+       "<title>16&#45;&gt;18</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M151.49,-285.21C141.01,-296.94 126.82,-312.83 115.3,-325.73\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"112.55\" cy=\"-328.8\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- o0 -->\n",
+       "<g id=\"node7\" class=\"node\">\n",
+       "<title>o0</title>\n",
+       "<polygon fill=\"#ffe5f1\" stroke=\"black\" points=\"95.2,-407.98 127.69,-442.48 62.7,-442.48 95.2,-407.98\"/>\n",
+       "<text text-anchor=\"middle\" x=\"95.2\" y=\"-427.28\" font-family=\"Times,serif\" font-size=\"14.00\">x</text>\n",
+       "</g>\n",
+       "<!-- 18&#45;&gt;o0 -->\n",
+       "<g id=\"edge1\" class=\"edge\">\n",
+       "<title>18&#45;&gt;o0:s</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M95.2,-372.17C95.2,-379.93 95.2,-388.92 95.2,-397.76\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"91.7,-397.98 95.2,-407.98 98.7,-397.98 91.7,-397.98\"/>\n",
+       "</g>\n",
+       "<!-- L0 -->\n",
+       "<g id=\"node6\" class=\"node\">\n",
+       "<title>L0</title>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"388.7,-122.75 333.7,-122.75 333.7,-86.75 388.7,-86.75 388.7,-122.75\"/>\n",
+       "<text text-anchor=\"middle\" x=\"361.2\" y=\"-101.05\" font-family=\"Times,serif\" font-size=\"14.00\">L0_in</text>\n",
+       "</g>\n",
+       "<!-- 2 -->\n",
+       "<g id=\"node8\" class=\"node\">\n",
+       "<title>2</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"284.2,-46 251.7,-11.5 316.69,-11.5 284.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"284.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">a</text>\n",
+       "</g>\n",
+       "<!-- 2&#45;&gt;16 -->\n",
+       "<g id=\"edge8\" class=\"edge\">\n",
+       "<title>2&#45;&gt;16</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M277.64,-39.04C263.71,-70.78 229.83,-146.8 198.2,-208.99 192.9,-219.41 186.74,-230.7 181.25,-240.5\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"179.17\" cy=\"-244.19\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 4 -->\n",
+       "<g id=\"node9\" class=\"node\">\n",
+       "<title>4</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"200.2,-46 166.6,-11.5 233.79,-11.5 200.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"200.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">b</text>\n",
+       "</g>\n",
+       "<!-- 4&#45;&gt;14 -->\n",
+       "<g id=\"edge6\" class=\"edge\">\n",
+       "<title>4&#45;&gt;14</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M196.36,-42.18C190.54,-69.82 179.39,-122.68 172.4,-155.83\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"171.54\" cy=\"-159.89\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 6 -->\n",
+       "<g id=\"node10\" class=\"node\">\n",
+       "<title>6</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"31.2,-46 -0.2,-11.5 62.59,-11.5 31.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"31.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">c</text>\n",
+       "</g>\n",
+       "<!-- 6&#45;&gt;12 -->\n",
+       "<g id=\"edge4\" class=\"edge\">\n",
+       "<title>6&#45;&gt;12</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M43.18,-33.46C59.21,-46.12 87.99,-68.84 108.49,-85.03\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"111.68\" cy=\"-87.55\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 8 -->\n",
+       "<g id=\"node11\" class=\"node\">\n",
+       "<title>8</title>\n",
+       "<polygon fill=\"#e9f4fb\" stroke=\"black\" points=\"114.2,-46 80.6,-11.5 147.79,-11.5 114.2,-46\"/>\n",
+       "<text text-anchor=\"middle\" x=\"114.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">d</text>\n",
+       "</g>\n",
+       "<!-- 8&#45;&gt;12 -->\n",
+       "<g id=\"edge3\" class=\"edge\">\n",
+       "<title>8&#45;&gt;12</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M118.28,-42.1C120.43,-51.62 123.12,-63.53 125.56,-74.34\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"126.48\" cy=\"-78.43\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "<!-- 0 -->\n",
+       "<g id=\"node12\" class=\"node\">\n",
+       "<title>0</title>\n",
+       "<polygon fill=\"#ffe6cc\" stroke=\"black\" points=\"388.2,-41 334.2,-41 334.2,-5 388.2,-5 388.2,-41\"/>\n",
+       "<text text-anchor=\"middle\" x=\"361.2\" y=\"-19.3\" font-family=\"Times,serif\" font-size=\"14.00\">False</text>\n",
+       "</g>\n",
+       "<!-- 0&#45;&gt;L0 -->\n",
+       "<g id=\"edge2\" class=\"edge\">\n",
+       "<title>0&#45;&gt;L0</title>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M361.2,-41.3C361.2,-52.07 361.2,-66.1 361.2,-78.14\"/>\n",
+       "<ellipse fill=\"black\" stroke=\"black\" cx=\"361.2\" cy=\"-82.48\" rx=\"4\" ry=\"4\"/>\n",
+       "</g>\n",
+       "</g>\n",
+       "</svg>\n"
+      ],
+      "text/plain": [
+       "<spot.aig; proxy of <Swig Object of type 'spot::aig_ptr *' at 0x7fbccc33adb0> >"
+      ]
+     },
+     "execution_count": 28,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "aig = spot.mealy_machine_to_aig(ctrl, \"ite\")\n",
+    "aig"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "f3b2d981",
+   "id": "eb81b7d3",
    "metadata": {},
    "outputs": [],
    "source": []