diff --git a/NEWS b/NEWS
index ca0f9904c..b34463943 100644
--- a/NEWS
+++ b/NEWS
@@ -93,6 +93,10 @@ New in spot 2.3.3.dev (not yet released)
   - ltldo and ltlcross could leave temporary files behind when
     aborting on error.
 
+  - The LTL simplifcation rule that turns F(f)|q into F(f|q)
+    when q is a subformula that is both eventual and universal
+    was documented but not applied in some forgotten cases.
+
   Backward-incompatible changes:
 
   - spot::acc_cond::mark_t::operator bool() has been marked as
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index af5b2e225..3c03666fe 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
-// Recherche et Developpement de l'Epita (LRDE).
+// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -698,7 +698,7 @@ namespace spot
       {
         bool e = f.is_eventual();
         bool u = f.is_universal();
-        bool eu = res_EventUniv && e & u && c_->options.favor_event_univ;
+        bool eu = res_EventUniv && e & u && c_->options.event_univ;
         switch (f.kind())
           {
           case op::X:
@@ -2137,30 +2137,24 @@ namespace spot
                       vec eu;
                       bool seen_g = false;
                       for (auto f: *s.res_EventUniv)
-                        {
-                          if (f.is_eventual() && f.is_universal())
-                            {
-                              if (f.is(op::G))
-                                {
-                                  seen_g = true;
-                                  eu.emplace_back(f[0]);
-                                }
-                              else
-                                {
-                                  eu.emplace_back(f);
-                                }
-                            }
-                          else
-                            {
-                              s.res_other->emplace_back(f);
-                            }
-                        }
+                        if (f.is(op::G))
+                          {
+                            seen_g = true;
+                            eu.emplace_back(f[0]);
+                          }
+                        else
+                          {
+                            eu.emplace_back(f);
+                          }
                       if (seen_g)
                         {
                           eu.emplace_back(allFG);
                           allFG = nullptr;
-                          s.res_other->emplace_back(unop_multop(op::G, op::And,
-                                                             eu));
+                          formula andeu = formula::multop(op::And, eu);
+                          if (!opt_.favor_event_univ)
+                            s.res_G->emplace_back(andeu);
+                          else
+                            s.res_other->emplace_back(formula::G(andeu));
                         }
                       else
                         {
@@ -2673,6 +2667,11 @@ namespace spot
                   formula allGF = unop_unop_multop(op::G, op::F, op::Or,
                                                    std::move(*s.res_GF));
 
+                  bool eu_has_F = false;
+                  for (auto f: *s.res_EventUniv)
+                    if (f.is(op::F))
+                      eu_has_F = true;
+
                   // Xa | Xb = X(a | b)
                   // Xa | Xb | GF(c) = X(a | b | GF(c))
                   // For Universal&Eventual formula f1...fn we also have:
@@ -2686,7 +2685,7 @@ namespace spot
                                       s.res_EventUniv->end());
                     }
                   else if (!opt_.favor_event_univ
-                           && !s.res_F->empty()
+                           && (!s.res_F->empty() || eu_has_F)
                            && s.res_G->empty()
                            && s.res_U_or_W->empty()
                            && s.res_R_or_M->empty()
@@ -2715,9 +2714,8 @@ namespace spot
                       // these differences)
                       s.res_F->emplace_back(allGF);
                       allGF = nullptr;
-                      s.res_F->insert(s.res_F->end(),
-                                      s.res_EventUniv->begin(),
-                                      s.res_EventUniv->end());
+                      for (auto f: *s.res_EventUniv)
+                        s.res_F->emplace_back(f.is(op::F) ? f[0] : f);
                     }
                   else if (opt_.favor_event_univ)
                     {
@@ -2726,7 +2724,7 @@ namespace spot
                       bool seen_f = false;
                       if (s.res_EventUniv->size() > 1)
                         {
-                          // If some of the EventUniv formulae start
+                          // If some of the EventUniv formulas start
                           // with an F, Gather them all under the
                           // same F.  Striping any leading F.
                           for (auto& f: *s.res_EventUniv)
@@ -2750,9 +2748,13 @@ namespace spot
                     }
                   else
                     {
-                      s.res_other->insert(s.res_other->end(),
-                                          s.res_EventUniv->begin(),
-                                          s.res_EventUniv->end());
+                      for (auto f: *s.res_EventUniv)
+                        {
+                          if (f.is(op::F))
+                            s.res_F->emplace_back(f[0]);
+                          else
+                            s.res_other->emplace_back(f);
+                        }
                     }
                   // Xa | Xb | f1...fn = X(a | b | f1...fn)
                   // is built at the end of this multop::Or case.
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index 82fa422fe..c9bd08a22 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -272,7 +272,7 @@ p-patterns,20, 1,8, 1,8, 3,24, 3,24
 !sb-patterns,5, 2,7, 2,7, 3,12, 3,12
 !sb-patterns,6, 3,11, 4,14, 3,11, 4,14
 !sb-patterns,7, 4,16, 4,16, 4,16, 4,16
-!sb-patterns,9, 4,19, 4,19, 6,27, 6,27
+!sb-patterns,9, 3,13, 3,13, 5,21, 5,21
 !sb-patterns,10, 2,6, 2,6, 2,6, 2,6
 !sb-patterns,11, 1,0, 1,0, 1,0, 1,0
 !sb-patterns,12, 1,0, 1,0, 1,0, 1,0
diff --git a/tests/core/reduccmp.test b/tests/core/reduccmp.test
index 7188a79ea..74308ecba 100755
--- a/tests/core/reduccmp.test
+++ b/tests/core/reduccmp.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2016 Laboratoire de
-# Recherche et Developpement de l'Epita (LRDE).
+# Copyright (C) 2009-2014, 2016-2017 Laboratoire de Recherche et
+# Developpement de l'Epita (LRDE).
 # Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -179,7 +179,8 @@ G(a | GFb), Ga | GFb
 F(a & GFb & c), F(a & GFb & c)
 G(a | GFb | c), G(a | c) | GFb
 
-GFa <=> GFb, G(Fa&Fb)|FG(!a&!b)
+GFa <=> GFb, F(G(Fa&Fb)|G(!a&!b))
+FGa | (GFa & GFb), F(Ga | (G(Fa & Fb)))
 
 Gb W a, Gb|a
 Fb M Fa, Fa & Fb
diff --git a/tests/python/atva16-fig2a.ipynb b/tests/python/atva16-fig2a.ipynb
index 8e2b789aa..6fa7be833 100644
--- a/tests/python/atva16-fig2a.ipynb
+++ b/tests/python/atva16-fig2a.ipynb
@@ -15,7 +15,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.5.2rc1"
+   "version": "3.5.3"
   },
   "name": ""
  },
@@ -86,113 +86,96 @@
         "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
         " -->\n",
         "<!-- Title: G Pages: 1 -->\n",
-        "<svg width=\"288pt\" height=\"360pt\"\n",
-        " viewBox=\"0.00 0.00 288.47 360.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
-        "<g id=\"graph0\" class=\"graph\" transform=\"scale(0.947368 0.947368) rotate(0) translate(4 376)\">\n",
+        "<svg width=\"198pt\" height=\"342pt\"\n",
+        " viewBox=\"0.00 0.00 197.50 342.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 1) rotate(0) translate(4 338)\">\n",
         "<title>G</title>\n",
-        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-376 300.5,-376 300.5,4 -4,4\"/>\n",
-        "<text text-anchor=\"start\" x=\"100.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
-        "<text text-anchor=\"start\" x=\"124.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"137.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
-        "<text text-anchor=\"start\" x=\"177.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
-        "<text text-anchor=\"start\" x=\"190.25\" y=\"-357.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
+        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-338 193.5,-338 193.5,4 -4,4\"/>\n",
+        "<text text-anchor=\"start\" x=\"47.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
+        "<text text-anchor=\"start\" x=\"69.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"85.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
+        "<text text-anchor=\"start\" x=\"121.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "<text text-anchor=\"start\" x=\"137.75\" y=\"-319.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
         "<!-- I -->\n",
-        "<!-- 0 -->\n",
-        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-105\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"56\" y=\"-101.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
-        "</g>\n",
-        "<!-- I&#45;&gt;0 -->\n",
-        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-105C2.79388,-105 17.1543,-105 30.6317,-105\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-105 30.9419,-108.15 34.4419,-105 30.9419,-105 30.9419,-105 30.9419,-105 34.4419,-105 30.9418,-101.85 37.9419,-105 37.9419,-105\"/>\n",
-        "</g>\n",
         "<!-- 1 -->\n",
-        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144.5\" cy=\"-156\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"144.5\" y=\"-152.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<g id=\"node2\" class=\"node\"><title>1</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-156\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-152.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
         "</g>\n",
-        "<!-- 0&#45;&gt;1 -->\n",
-        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M72.0672,-113.884C85.9591,-122.074 106.722,-134.316 122.288,-143.493\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"128.606,-147.218 120.976,-146.376 125.591,-145.441 122.576,-143.663 122.576,-143.663 122.576,-143.663 125.591,-145.441 124.175,-140.95 128.606,-147.218 128.606,-147.218\"/>\n",
-        "<text text-anchor=\"middle\" x=\"97\" y=\"-133.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<!-- I&#45;&gt;1 -->\n",
+        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-156C2.79388,-156 17.1543,-156 30.6317,-156\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-156 30.9419,-159.15 34.4419,-156 30.9419,-156 30.9419,-156 30.9419,-156 34.4419,-156 30.9418,-152.85 37.9419,-156 37.9419,-156\"/>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;1 -->\n",
+        "<g id=\"edge4\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-173.037C48.3189,-182.858 50.4453,-192 56,-192 60.166,-192 62.4036,-186.858 62.7128,-180.143\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-173.037 65.8541,-179.882 62.5434,-176.533 62.7076,-180.03 62.7076,-180.03 62.7076,-180.03 62.5434,-176.533 59.561,-180.177 62.3792,-173.037 62.3792,-173.037\"/>\n",
+        "<text text-anchor=\"middle\" x=\"56\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "</g>\n",
+        "<!-- 0 -->\n",
+        "<g id=\"node3\" class=\"node\"><title>0</title>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"169\" cy=\"-247\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"169\" y=\"-243.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
+        "</g>\n",
+        "<!-- 1&#45;&gt;0 -->\n",
+        "<g id=\"edge3\" class=\"edge\"><title>1&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M70.6108,-167.158C90.2734,-183.278 126.706,-213.147 149.007,-231.429\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"154.625,-236.035 147.214,-234.033 151.918,-233.816 149.211,-231.597 149.211,-231.597 149.211,-231.597 151.918,-233.816 151.208,-229.161 154.625,-236.035 154.625,-236.035\"/>\n",
+        "<text text-anchor=\"start\" x=\"92\" y=\"-220.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
         "</g>\n",
         "<!-- 2 -->\n",
         "<g id=\"node4\" class=\"node\"><title>2</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"272\" cy=\"-76\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"272\" y=\"-72.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
+        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"169\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
+        "<text text-anchor=\"middle\" x=\"169\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
         "</g>\n",
-        "<!-- 0&#45;&gt;2 -->\n",
-        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M74.1508,-102.676C112.123,-97.5301 203.374,-85.1643 246.992,-79.2534\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"254.065,-78.295 247.551,-82.3565 250.596,-78.765 247.128,-79.2351 247.128,-79.2351 247.128,-79.2351 250.596,-78.765 246.705,-76.1136 254.065,-78.295 254.065,-78.295\"/>\n",
-        "<text text-anchor=\"start\" x=\"120\" y=\"-99.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<!-- 1&#45;&gt;2 -->\n",
+        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M68.0489,-142.264C87.9125,-117.568 129.699,-65.6173 152.446,-37.3378\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"156.996,-31.6809 155.063,-39.1098 154.802,-34.4082 152.608,-37.1354 152.608,-37.1354 152.608,-37.1354 154.802,-34.4082 150.154,-35.1611 156.996,-31.6809 156.996,-31.6809\"/>\n",
+        "<text text-anchor=\"start\" x=\"99\" y=\"-114.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
         "</g>\n",
-        "<!-- 3 -->\n",
-        "<g id=\"node5\" class=\"node\"><title>3</title>\n",
-        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"144.5\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
-        "<text text-anchor=\"middle\" x=\"144.5\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">3</text>\n",
+        "<!-- 0&#45;&gt;0 -->\n",
+        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M159.425,-262.541C156.73,-272.909 159.922,-283 169,-283 175.95,-283 179.45,-277.085 179.499,-269.659\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"178.575,-262.541 182.6,-269.077 179.026,-266.012 179.477,-269.483 179.477,-269.483 179.477,-269.483 179.026,-266.012 176.353,-269.889 178.575,-262.541 178.575,-262.541\"/>\n",
+        "<text text-anchor=\"start\" x=\"148.5\" y=\"-300.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"153\" y=\"-286.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"169\" y=\"-286.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
         "</g>\n",
-        "<!-- 0&#45;&gt;3 -->\n",
-        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M69.3933,-92.535C84.1669,-77.676 108.963,-52.7363 125.764,-35.8381\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"131.13,-30.4419 128.428,-37.6268 128.662,-32.9239 126.194,-35.4059 126.194,-35.4059 126.194,-35.4059 128.662,-32.9239 123.96,-33.1849 131.13,-30.4419 131.13,-30.4419\"/>\n",
-        "<text text-anchor=\"middle\" x=\"97\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge6\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M166.467,-36.1527C166.078,-45.5391 166.922,-54 169,-54 170.526,-54 171.387,-49.437 171.582,-43.2953\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"171.533,-36.1527 174.731,-43.1307 171.557,-39.6526 171.581,-43.1525 171.581,-43.1525 171.581,-43.1525 171.557,-39.6526 168.431,-43.1743 171.533,-36.1527 171.533,-36.1527\"/>\n",
+        "<text text-anchor=\"start\" x=\"150.5\" y=\"-72.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"161\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
         "</g>\n",
-        "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M142.42,-174.153C142.099,-183.539 142.793,-192 144.5,-192 145.754,-192 146.461,-187.437 146.621,-181.295\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"146.58,-174.153 149.77,-181.135 146.6,-177.653 146.62,-181.153 146.62,-181.153 146.62,-181.153 146.6,-177.653 143.47,-181.171 146.58,-174.153 146.58,-174.153\"/>\n",
-        "<text text-anchor=\"start\" x=\"123\" y=\"-210.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
-        "<text text-anchor=\"start\" x=\"138\" y=\"-195.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge7\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M165.104,-35.5771C162.424,-56.718 163.723,-84 169,-84 173.7,-84 175.244,-62.3596 173.633,-42.6907\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"172.896,-35.5771 176.75,-42.2155 173.257,-39.0585 173.617,-42.5399 173.617,-42.5399 173.617,-42.5399 173.257,-39.0585 170.484,-42.8644 172.896,-35.5771 172.896,-35.5771\"/>\n",
+        "<text text-anchor=\"start\" x=\"148.5\" y=\"-87.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
         "</g>\n",
-        "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M141.266,-173.906C139.109,-195 140.188,-222 144.5,-222 148.341,-222 149.616,-200.583 148.326,-180.997\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"147.734,-173.906 151.455,-180.62 148.025,-177.394 148.316,-180.882 148.316,-180.882 148.316,-180.882 148.025,-177.394 145.177,-181.144 147.734,-173.906 147.734,-173.906\"/>\n",
-        "<text text-anchor=\"start\" x=\"120\" y=\"-225.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M140.372,-173.871C136.217,-201.525 137.593,-240 144.5,-240 150.84,-240 152.52,-207.578 149.539,-180.868\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"148.628,-173.871 152.655,-180.406 149.08,-177.342 149.532,-180.812 149.532,-180.812 149.532,-180.812 149.08,-177.342 146.408,-181.219 148.628,-173.871 148.628,-173.871\"/>\n",
-        "<text text-anchor=\"start\" x=\"126\" y=\"-257.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
-        "<text text-anchor=\"start\" x=\"131.5\" y=\"-243.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"144.5\" y=\"-243.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
-        "</g>\n",
-        "<!-- 1&#45;&gt;1 -->\n",
-        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M139.905,-173.612C133.288,-209.893 134.819,-268 144.5,-268 153.576,-268 155.489,-216.929 150.24,-180.651\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"149.095,-173.612 153.328,-180.015 149.657,-177.067 150.219,-180.521 150.219,-180.521 150.219,-180.521 149.657,-177.067 147.11,-181.027 149.095,-173.612 149.095,-173.612\"/>\n",
-        "<text text-anchor=\"start\" x=\"123\" y=\"-286.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
-        "<text text-anchor=\"start\" x=\"138\" y=\"-271.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<!-- 2&#45;&gt;2 -->\n",
+        "<g id=\"edge8\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M164.049,-35.4671C158.901,-63.1487 160.551,-102 169,-102 176.756,-102 178.783,-69.2613 175.081,-42.4773\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"173.951,-35.4671 178.174,-41.8767 174.508,-38.9225 175.065,-42.3779 175.065,-42.3779 175.065,-42.3779 174.508,-38.9225 171.955,-42.8792 173.951,-35.4671 173.951,-35.4671\"/>\n",
+        "<text text-anchor=\"start\" x=\"152\" y=\"-119.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
+        "<text text-anchor=\"start\" x=\"153\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
+        "<text text-anchor=\"start\" x=\"169\" y=\"-105.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
         "</g>\n",
         "<!-- 2&#45;&gt;2 -->\n",
         "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M261.849,-91.1666C258.772,-101.664 262.156,-112 272,-112 279.537,-112 283.287,-105.941 283.25,-98.39\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"282.151,-91.1666 286.318,-97.6135 282.678,-94.6269 283.204,-98.0871 283.204,-98.0871 283.204,-98.0871 282.678,-94.6269 280.09,-98.5607 282.151,-91.1666 282.151,-91.1666\"/>\n",
-        "<text text-anchor=\"start\" x=\"247.5\" y=\"-129.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
-        "<text text-anchor=\"start\" x=\"259\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
-        "<text text-anchor=\"start\" x=\"272\" y=\"-115.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#f17cb0\">\u2776</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;2 -->\n",
-        "<g id=\"edge10\" class=\"edge\"><title>3&#45;&gt;2</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M161.141,-25.2285C183.217,-35.4311 223.626,-54.1061 248.802,-65.741\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"255.162,-68.6804 247.486,-68.6032 251.985,-67.2121 248.808,-65.7438 248.808,-65.7438 248.808,-65.7438 251.985,-67.2121 250.129,-62.8844 255.162,-68.6804 255.162,-68.6804\"/>\n",
-        "<text text-anchor=\"start\" x=\"187\" y=\"-61.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
-        "</g>\n",
-        "<!-- 3&#45;&gt;3 -->\n",
-        "<g id=\"edge11\" class=\"edge\"><title>3&#45;&gt;3</title>\n",
-        "<path fill=\"none\" stroke=\"black\" d=\"M136.484,-34.2903C134.551,-44.3892 137.223,-54 144.5,-54 149.958,-54 152.826,-48.5939 153.103,-41.6304\"/>\n",
-        "<polygon fill=\"black\" stroke=\"black\" points=\"152.516,-34.2903 156.214,-41.0172 152.795,-37.7792 153.074,-41.268 153.074,-41.268 153.074,-41.268 152.795,-37.7792 149.934,-41.5189 152.516,-34.2903 152.516,-34.2903\"/>\n",
-        "<text text-anchor=\"middle\" x=\"144.5\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
+        "<path fill=\"none\" stroke=\"black\" d=\"M163.463,-35.3599C155.342,-71.623 157.188,-130 169,-130 180.074,-130 182.389,-78.6921 175.943,-42.3988\"/>\n",
+        "<polygon fill=\"black\" stroke=\"black\" points=\"174.537,-35.3599 178.997,-41.6073 175.223,-38.7921 175.908,-42.2243 175.908,-42.2243 175.908,-42.2243 175.223,-38.7921 172.819,-42.8414 174.537,-35.3599 174.537,-35.3599\"/>\n",
+        "<text text-anchor=\"start\" x=\"150.5\" y=\"-148.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
+        "<text text-anchor=\"start\" x=\"161\" y=\"-133.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#5da5da\">\u24ff</text>\n",
         "</g>\n",
         "</g>\n",
         "</svg>\n"
        ],
        "text": [
-        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f77f87ba300> >"
+        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f79506d2900> >"
        ]
       }
      ],