diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index c11702450..8947c9cfa 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -108,6 +108,9 @@
 
 % rewriting rules that enlarge the formula
 \newcommand{\equiV}{\stackrel{\star}{\equiv}}
+% rewriting rules that favors event/univ
+\newcommand{\equivEU}{\stackrel{\blacktriangleup}{\equiv}}
+\newcommand{\equivNeu}{\stackrel{\smalltriangledown}{\equiv}}
 
 % marked rewriting rules
 \newcommand{\equivM}{\stackrel{\dag}{\equiv}}
@@ -1298,6 +1301,13 @@ The goals in most of these simplification are to:
   limit the sources of indeterminism.
 \end{itemize}
 
+Rewritings defined with $\equivEU$ are applied only when
+\verb|ltl_simplifier_options::favor_event_univ|' is \texttt{true}:
+they try to lift subformulas that are both eventual and universal
+\emph{higher} in the syntax tree.  Conversely, rules defined with $\equivNeu$
+are applied only when \verb|favor_event_univ|' is \texttt{false}: they
+try to \textit{lower} subformulas that are both eventual and universal.
+
 \subsection{Basic Simplifications}\label{sec:basic-simp}
 
 These simplifications are enabled with
@@ -1356,10 +1366,10 @@ $\OR$):
   (\G\F f) \OR (\G\F g) &\equiv \G\F(f\OR g)      \\
   (\X f) \AND(\X g)     &\equiv \X(f\AND g)       &
   (\X f) \OR (\X g)     &\equiv \X(f\OR g)        \\
-  (\X f) \AND(\F\G g)   &\equiv \X(f\AND \F\G g)  &
-  (\X f) \OR (\G\F g)   &\equiv \X(f\OR \G\F g)   \\
-  (\G f) \AND(\G g)     &\equiv \G(f\AND g)       &
-  (\F f) \OR (\F g)     &\equiv \F(f\OR g)        \\
+  (\X f) \AND(\F\G g)   &\equivNeu \X(f\AND \F\G g)  &
+  (\X f) \OR (\G\F g)   &\equivNeu \X(f\OR \G\F g)  \\
+  (\G f) \AND(\G g)     &\equivNeu \G(f\AND g)       &
+  (\F f) \OR (\F g)     &\equivNeu \F(f\OR g)        \\
   (f_1 \U f_2)\AND (f_3 \U f_2)&\equiv (f_1\AND f_3)\U f_2&
   (f_1 \U f_2)\OR  (f_1 \U f_3)&\equiv f_1\U (f_2\OR f_3) \\
   (f_1 \U f_2)\AND (f_3 \W f_2)&\equiv (f_1\AND f_3)\U f_2&
@@ -1409,8 +1419,8 @@ $b \OR c\OR \X(\F(a\OR b\OR c)\OR \G d)$.
 Finally the following rule is applied only when no other terms are present
 in the OR arguments:
 \begin{align*}
-  \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m)
-   &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots \OR g_m)) \\
+  \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g)
+   &\equivNeu \F(f_1\OR \ldots \OR f_n \OR \G\F(g)) \\
 \end{align*}
 
 \subsubsection{Basic Simplifications for SERE Operators}
@@ -1558,17 +1568,29 @@ $q,\,q_i$           & a pure eventuality that is also purely universal \\
 \end{center}
 
 \begin{align*}
-  \F e &\equiv e & f \U e &\equiv e & e \M f &\equiv e\AND f & u_1 \M u_2 &\equiV (\F u_1) \AND u_2 \\
-  \G u &\equiv u & f \R u &\equiv u &  u \W f &\equiv u\OR f & e_1 \W e_2 &\equiV (\G e_1) \OR e_2 \\
-  \X q &\equiv q & q \AND \X f &\equiv \X(q \AND f) & q\OR \X f &\equiv \X(q \OR f)
+  \F e        & \equiv e            & f \U e         & \equiv e                & e \M g        & \equiv e\AND g & u_1 \M u_2 & \equiV (\F u_1) \AND u_2 \\
+  \F(u)\OR q  & \equivEU \F(u\OR q) & f \U (g\OR e)  & \equivEU (f \U g)\OR e  & f\M (g\AND u) & \equivEU (f \M g)\AND u                                \\
+              &                     & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q                                \\
+  \G u        & \equiv u            & u \W g         & \equiv u\OR g           & f \R u        & \equiv u       & e_1 \W e_2 & \equiV (\G e_1) \OR e_2  \\
+  \G(e)\AND q & \equiv \G(e\AND q)  & f \W (g\OR e)  & \equivEU (f \W g)\OR e  & f\R (g\AND u) & \equivEU (f \R g)\AND u                                \\
+              &                     & (f\OR u) \W g  & \equivEU (f \W g)\OR u                                                                           \\
+  \X q        & \equiv q            & q \AND \X f    & \equivNeu \X(q \AND f)  & q\OR \X f     & \equivNeu \X(q \OR f)                                  \\
+              &                     & \X(q \AND f)   & \equivEU q \AND \X f    & \X(q \OR f)   & \equivEU q\OR \X f                                     \\
 \end{align*}
+
 \begin{align*}
-  \G(f_1\OR\ldots\OR f_n \OR \G\F(g_1)\OR\ldots\OR \G\F(g_m)\OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR \G\F(g_1\OR\ldots\OR g_m)\OR q_1 \OR \ldots q_p \\
+  \G(f_1\OR\ldots\OR f_n \OR q_1 \OR \ldots \OR q_p)&\equiv \G(f_1\OR\ldots\OR f_n)\OR q_1 \OR \ldots \OR q_p \\
+  \F(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \F(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
+  \G(f_1\AND\ldots\AND f_n \AND q_1 \AND \ldots \AND q_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND q_1 \AND \ldots \AND q_p \\
+  \G(f_1\AND\ldots\AND f_n \AND e_1 \AND \ldots \AND e_m \AND \G(e_{m+1}) \AND \ldots\AND \G(e_p))&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\
+  \G(f_1\AND\ldots\AND f_n \AND \G(g_1) \AND \ldots \AND \G(g_m) &\equiv \G(f_1\AND\ldots\AND f_n\AND g_1 \AND \ldots \AND g_m) \\
+  \F(f_1 \OR \ldots \OR f_n \OR u_1 \OR \ldots \OR u_m \OR \F(u_{m+1})\OR\ldots\OR \F(u_p)) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_p)\\
+  \F(f_1 \OR \ldots \OR f_n \OR \F(g_1) \OR \ldots \OR \G(g_m)) &\equiv \F(f_1\OR \ldots\OR f_n \OR g_1 \OR \ldots \OR g_m)\\
+  \G(f_1)\AND\ldots\AND \G(f_n) \AND \G(e_1) \AND \ldots\AND \G(e_p)&\equivEU \G(f_1\AND\ldots\AND f_n)\AND \G(e_1 \AND \ldots \AND e_p) \\
+  \F(f_1) \OR\ldots\OR \F(f_n) \OR \F(u_1)\OR\ldots\OR \F(u_p) &\equivEU \F(f_1\OR \ldots\OR f_n) \OR \F(u_1 \OR \ldots \OR u_p)\\
 \intertext{Finally the following rule is applied only when no other
     terms are present in the OR arguments:}
-  \F(f_1) \OR \ldots \OR \F(f_n) \OR \G\F(g_1) \OR \ldots \OR \G\F(g_m)
-  \OR q_1 \OR \ldots \OR q_p
-   &\equiv \F(f_1\OR \ldots \OR f_n \OR \G\F(g_1\OR \ldots\OR g_m) \OR q_1\OR \ldots q_p)
+  \F(f_1) \OR \ldots \OR \F(f_n) \OR q_1 \OR \ldots \OR q_p &\equivNeu \F(f_1\OR \ldots \OR f_n \OR q_1\OR \ldots q_p)
 \end{align*}
 
 \subsection{Simplifications Based on Implications}
diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index e985215bd..57b36b5f7 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -36,6 +36,7 @@ check_PROGRAMS = \
   nenoform \
   reduc \
   reduccmp \
+  reduceu \
   reductau \
   reductaustr \
   syntimpl \
@@ -58,6 +59,8 @@ nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
 reduc_SOURCES = reduc.cc
 reduccmp_SOURCES = equals.cc
 reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
+reduceu_SOURCES = equals.cc
+reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV
 reductau_SOURCES = equals.cc
 reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU
 reductaustr_SOURCES = equals.cc
@@ -99,7 +102,8 @@ TESTS = \
   reduc0.test \
   reducpsl.test \
   reduccmp.test \
-  uwrm.test
+  uwrm.test \
+  eventuniv.test
 
 distclean-local:
 	rm -rf $(TESTS:.test=.dir)
diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
index 6387fa604..a9b5905f9 100644
--- a/src/ltltest/equals.cc
+++ b/src/ltltest/equals.cc
@@ -104,6 +104,9 @@ main(int argc, char** argv)
 #endif
 #ifdef REDUC
     spot::ltl::ltl_simplifier_options opt(true, true, true, false, false);
+#  ifdef EVENT_UNIV
+    opt.favor_event_univ = true;
+#  endif
     spot::ltl::ltl_simplifier simp(opt);
     {
       const spot::ltl::formula* tmp;
diff --git a/src/ltltest/eventuniv.test b/src/ltltest/eventuniv.test
new file mode 100755
index 000000000..195322795
--- /dev/null
+++ b/src/ltltest/eventuniv.test
@@ -0,0 +1,60 @@
+#! /bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs || exit 1
+
+check()
+{
+  run 0 ../reduceu "$@"
+}
+
+check 'Xa | GFb'    'Xa | GFb'
+check 'X(a | GXFb)' 'Xa | GFb'
+check 'Xa & GFb'    'Xa & GFb'
+check 'X(a & GXFb)' 'Xa & GFb'
+
+check 'F(a & b & GFc & FGd)' 'F(a & b) & G(Fc & FGd)'
+check 'Fa | Fb | GFc | GFd' 'F(a|b) | GF(c | d)'
+check 'Fa | Fb | GFc | GFd | FGe' 'F(a|b) | F(G(e) | GF(c | d))'
+cehck 'Ga | Gb | GFd | FGe | FGf' 'Ga | Gb | F(GFd | Ge | Gf)'
+
+check 'G(Ga & Fb & c & GFd)'  'G(a&c) & G(Fb & Fd)'
+check 'G(Ga & GFb & c & GFd)' 'G(a&c) & G(Fb & Fd)'
+check 'G(a & GFb & c & GFd)'  'G(a&c) & G(Fb & Fd)'
+check 'G(Ga & Fb & c & GFd & FGe)' 'G(a & c) & G(Fb & Fd & FGe)'
+check 'G(Ga & XFGb & c & FGd & FGe)' 'FG(b & d & e) & G(a & c)'
+check 'G(Ga & GXFb & c & FGd & FGe & Fc)' 'G(Fb & FG(d & e)) & G(a & c)'
+check 'Ga & Gb & GFd & FGe & FGf'    'G(Fd & FG(e & f)) & G(a & b)'
+check 'G(Ga & Gb & GFd & FGe) & FGf' 'G(Fd & FG(e & f)) & G(a & b)'
+
+check 'a U (b | Fc)'  '(a U b) | Fc'
+check 'a W (b | Fc)'  '(a W b) | Fc'
+check 'a U (b & GFc)' '(a U b) & GFc'
+check 'a W (b & GFc)' 'a W (b & GFc)'  # Unchanged
+check '(a | Gc) W g'  '(a W g) | Gc'
+check '(a | Gc) U g'  '(a | Gc) U g'   # Unchanged
+
+check '(a & GFc) M b' '(a M b) & GFc'
+check '(a | GFc) M b' '(a | GFc) M b'  # Unchanged
+check '(a & GFc) R b' '(a & GFc) R b'  # Unchanged
+check '(a | GFc) R b' '(a | GFc) R b'  # Unchanged
+check 'a R (b & Gc)'  '(a R b) & Gc'
+check 'a M (b & Gc)'  '(a M b) & Gc'
+
diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc
index 368c30b47..2456e6fc3 100644
--- a/src/ltltest/reduc.cc
+++ b/src/ltltest/reduc.cc
@@ -134,6 +134,13 @@ main(int argc, char** argv)
       o.containment_checks = true;
       o.containment_checks_stronger = true;
       break;
+    case 15:
+      o.reduce_basics = true;
+      o.event_univ = true;
+      o.containment_checks = true;
+      o.containment_checks_stronger = true;
+      o.favor_event_univ = true;
+      break;
     default:
       return 2;
   }
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 873db091a..633346faf 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -129,6 +129,7 @@ namespace spot
 	: dict(d), options(opt), lcc(d, true, true, false, false)
       {
 	options.containment_checks |= options.containment_checks_stronger;
+	options.event_univ |= options.favor_event_univ;
       }
 
       void
@@ -880,6 +881,9 @@ namespace spot
 
 	void process(const formula* f)
 	{
+	  bool e = f->is_eventual();
+	  bool u = f->is_universal();
+	  bool eu = res_EventUniv && e & u && c_->options.favor_event_univ;
 	  switch (f->kind())
 	    {
 	    case formula::UnOp:
@@ -889,21 +893,21 @@ namespace spot
 		switch (uo->op())
 		  {
 		  case unop::X:
-		    if (res_X)
+		    if (res_X && !eu)
 		      {
 			res_X->push_back(c->clone());
 			return;
 		      }
 		    break;
 		  case unop::F:
-		    if (res_FG)
+		    if (res_FG && u)
 		      if (const unop* cc = is_G(c))
 			{
 			  res_FG->push_back(((split_ & Strip_FG) == Strip_FG
 					     ? cc->child() : f)->clone());
 			  return;
 			}
-		    if (res_F)
+		    if (res_F && !eu)
 		      {
 			res_F->push_back(((split_ & Strip_F) == Strip_F
 					  ? c : f)->clone());
@@ -911,14 +915,14 @@ namespace spot
 		      }
 		    break;
 		  case unop::G:
-		    if (res_GF)
+		    if (res_GF && e)
 		      if (const unop* cc = is_F(c))
 			{
 			  res_GF->push_back(((split_ & Strip_GF) == Strip_GF
 					     ? cc->child() : f)->clone());
 			  return;
 			}
-		    if (res_G)
+		    if (res_G && !eu)
 		      {
 			res_G->push_back(((split_ & Strip_G) == Strip_G
 					  ? c : f)->clone());
@@ -966,8 +970,6 @@ namespace spot
 	    }
 	  if (c_->options.event_univ)
 	    {
-	      bool e = f->is_eventual();
-	      bool u = f->is_universal();
 	      if (res_EventUniv && e && u)
 		{
 		  res_EventUniv->push_back(f->clone());
@@ -1154,12 +1156,28 @@ namespace spot
 		  && c_->lcc.equal(result_, uo))
 		return;
 
-	      // Disabled: X(f1 & GF(f2)) = X(f1) & GF(f2)
-	      // Disabled: X(f1 | GF(f2)) = X(f1) | GF(f2)
-	      // Disabled: X(f1 & FG(f2)) = X(f1) & FG(f2)
-	      // Disabled: X(f1 | FG(f2)) = X(f1) | FG(f2)
-	      // The above make more sense when reversed,
-	      // so see them in the And and Or rewritings.
+	      // X(f1 & GF(f2)) = X(f1) & GF(f2)
+	      // X(f1 | GF(f2)) = X(f1) | GF(f2)
+	      // X(f1 & FG(f2)) = X(f1) & FG(f2)
+	      // X(f1 | FG(f2)) = X(f1) | FG(f2)
+	      //
+	      // The above usually make more sense when reversed (see
+	      // them in the And and Or rewritings), except when we
+	      // try to maximaze the size of subformula that do not
+	      // have EventUniv formulae.
+	      if (opt_.favor_event_univ)
+		if (const multop* mo = is_multop(result_,
+						 multop::Or, multop::And))
+		  {
+		    mospliter s(mospliter::Split_EventUniv, mo, c_);
+		    multop::type op = mo->op();
+		    s.res_EventUniv->push_back(unop_multop(unop::X, op,
+							   s.res_other));
+		    result_ = multop::instance(op, s.res_EventUniv);
+		    if (result_ != uo)
+		      result_ = recurse_destroy(result_);
+		    return;
+		  }
 	      break;
 
 	    case unop::F:
@@ -1259,7 +1277,8 @@ namespace spot
 		  && c_->lcc.contained(uo, result_))
 		return;
 
-	      // Disabled: F(f1 & GF(f2)) = F(f1) & GF(f2)
+	      // Disabled by default:
+	      //     F(f1 & GF(f2)) = F(f1) & GF(f2)
 	      //
 	      // As is, these two formulae are translated into
 	      // equivalent Büchi automata so the rewriting is
@@ -1272,7 +1291,86 @@ namespace spot
 	      // rule which really helps the translation. F((f1 &
 	      // GF(f2)) | (a & GF(b))) is indeed easier to translate.
 	      //
-	      // So let's not consider this rewriting rule.
+	      // So we do not consider this rewriting rule by default.
+	      // However if favor_event_univ is set, we want to move
+	      // the GF out of the F.
+	      if (opt_.favor_event_univ)
+		// F(f1&f2&FG(f3)&FG(f4)&f5&f6) =
+		//                        F(f1&f2) & FG(f3&f4) & f5 & f6
+		// if f5 and f6 are both eventual and universal.
+		if (const multop* mo = is_And(result_))
+		  {
+		    mo->clone();
+		    mospliter s(mospliter::Strip_FG |
+				mospliter::Split_EventUniv,
+				mo, c_);
+		    s.res_EventUniv->
+		      push_back(unop_multop(unop::F, multop::And,
+					    s.res_other));
+		    s.res_EventUniv->
+		      push_back(unop_unop_multop(unop::F, unop::G,
+						 multop::And, s.res_FG));
+		    result_ = multop::instance(multop::And, s.res_EventUniv);
+		    if (result_ != uo)
+		      {
+			mo->destroy();
+			result_ = recurse_destroy(result_);
+			return;
+		      }
+		    else
+		      {
+			// Revert to the previous value of result_,
+			// for the next simplification.
+			result_->destroy();
+			result_ = mo;
+		      }
+		  }
+	      // If u3 and u4 are universal formulae and h is not:
+	      // F(f1 | f2 | Fu3 | u4 | FGg | Fh)
+	      //    = F(f1 | f2 | u3 | u4 | Gg | h)
+	      // or
+	      // F(f1 | f2 | Fu3 | u4 | FGg | Fh)
+	      //    = F(f1 | f2 | h) | F(u3 | u4 | Gg)
+	      // depending on whether favor_event_univ is set.
+	      if (const multop* mo = is_Or(result_))
+		{
+		  mo->clone();
+		  int w = mospliter::Strip_F;
+		  if (opt_.favor_event_univ)
+		    w |= mospliter::Split_Univ;
+		  mospliter s(w, mo, c_);
+		  s.res_other->insert(s.res_other->end(),
+				      s.res_F->begin(), s.res_F->end());
+		  delete s.res_F;
+		  result_ = unop_multop(unop::F, multop::Or, s.res_other);
+		  if (s.res_Univ)
+		    {
+		      // Strip any F.
+		      for (multop::vec::iterator i = s.res_Univ->begin();
+			   i != s.res_Univ->end(); ++i)
+			if (const unop* u = is_F(*i))
+			  {
+			    *i = u->child()->clone();
+			    u->destroy();
+			  }
+		      const formula* fu =
+			unop_multop(unop::F, multop::Or, s.res_Univ);
+		      result_ = multop::instance(multop::Or, result_, fu);
+		    }
+		  if (result_ != uo)
+		    {
+		      mo->destroy();
+		      result_ = recurse_destroy(result_);
+		      return;
+		    }
+		  else
+		    {
+		      // Revert to the previous value of result_,
+		      // for the next simplification.
+		      result_->destroy();
+		      result_ = mo;
+		    }
+		}
 	      break;
 
 	    case unop::G:
@@ -1356,6 +1454,52 @@ namespace spot
 			  result_ = mo;
 			}
 		    }
+		  // If e3 and e4 are eventual formulae and h is not:
+		  // G(f1 & f2 & Ge3 & e4 & GFg & Gh)
+		  //    = G(f1 & f2 & e3 & e4 & Fg & h)
+		  // or
+		  // G(f1 & f2 & Ge3 & e4 & GFg & Gh)
+		  //    = G(f1 & f2 & h) & G(e3 & e4 & Fg)
+		  // depending on whether favor_event_univ is set.
+		  else if (const multop* mo = is_And(result_))
+		    {
+		      mo->clone();
+		      int w = mospliter::Strip_G;
+		      if (opt_.favor_event_univ)
+			w |= mospliter::Split_Event;
+		      mospliter s(w, mo, c_);
+		      s.res_other->insert(s.res_other->end(),
+					  s.res_G->begin(), s.res_G->end());
+		      delete s.res_G;
+		      result_ = unop_multop(unop::G, multop::And, s.res_other);
+		      if (s.res_Event)
+			{
+			  // Strip any G.
+			  for (multop::vec::iterator i = s.res_Event->begin();
+			       i != s.res_Event->end(); ++i)
+			    if (const unop* u = is_G(*i))
+			      {
+				*i = u->child()->clone();
+				u->destroy();
+			      }
+			  const formula* ge =
+			    unop_multop(unop::G, multop::And, s.res_Event);
+			  result_ = multop::instance(multop::And, result_, ge);
+			}
+		      if (result_ != uo)
+			{
+			  mo->destroy();
+			  result_ = recurse_destroy(result_);
+			  return;
+			}
+		      else
+			{
+			  // Revert to the previous value of result_,
+			  // for the next simplification.
+			  result_->destroy();
+			  result_ = mo;
+			}
+		    }
 
 		  // GF(a | Xb) = GF(a | b)
 		  // GF(a | Fb) = GF(a | b)
@@ -1870,7 +2014,6 @@ namespace spot
 		  return;
 		}
 
-
 	      // e₁ W e₂ = Ge₁ | e₂
 	      // u₁ M u₂ = Fu₁ & u₂
 	      if (!opt_.reduce_size_strictly)
@@ -1893,6 +2036,113 @@ namespace spot
 		    }
 		}
 
+	      // In the following rewritings we assume that
+	      // - e is a pure eventuality
+	      // - u is purely universal
+	      // - q is purely universal pure eventuality
+	      // (a U (b|e)) = (a U b)|e
+	      // (a W (b|e)) = (a W b)|e
+	      // (a U (b&q)) = (a U b)&q
+	      // ((a&q) M b) = (a M b)&q
+	      // ((a|u) W b) = u|(a W b)
+	      // (a R (b&u)) = (a R b)&u
+	      // (a M (b&u)) = (a M b)&u
+	      if (opt_.favor_event_univ)
+		{
+		  if (op == binop::U || op == binop::W)
+		    if (const multop* mo = is_Or(b))
+		      {
+			b->clone();
+			mospliter s(mospliter::Split_Event, mo, c_);
+			const formula* b2 =
+			  multop::instance(multop::Or, s.res_other);
+			if (b2 != b)
+			  {
+			    b->destroy();
+			    s.res_Event->push_back(binop::instance(op, a, b2));
+			    result_ =
+			      recurse_destroy(multop::instance(multop::Or,
+							       s.res_Event));
+			    return;
+			  }
+			b2->destroy();
+			delete s.res_Event;
+		      }
+		  if (op == binop::W)
+		    if (const multop* mo = is_Or(a))
+		      {
+			a->clone();
+			mospliter s(mospliter::Split_Univ, mo, c_);
+			const formula* a2 =
+			  multop::instance(multop::Or, s.res_other);
+			if (a2 != a)
+			  {
+			    a->destroy();
+			    s.res_Univ->push_back(binop::instance(op, a2, b));
+			    result_ = recurse_destroy
+			      (multop::instance(multop::Or, s.res_Univ));
+			    return;
+			  }
+			a2->destroy();
+			delete s.res_Univ;
+		      }
+		  if (op == binop::U)
+		    if (const multop* mo = is_And(b))
+		      {
+			b->clone();
+			mospliter s(mospliter::Split_EventUniv, mo, c_);
+			const formula* b2 =
+			  multop::instance(multop::And, s.res_other);
+			if (b2 != b)
+			  {
+			    b->destroy();
+			    s.res_EventUniv->push_back(binop::instance(op,
+								       a, b2));
+			    result_ = recurse_destroy
+			      (multop::instance(multop::And, s.res_EventUniv));
+			    return;
+			  }
+			b2->destroy();
+			delete s.res_Event;
+		      }
+		  if (op == binop::M)
+		    if (const multop* mo = is_And(a))
+		      {
+			a->clone();
+			mospliter s(mospliter::Split_EventUniv, mo, c_);
+			const formula* a2 =
+			  multop::instance(multop::And, s.res_other);
+			if (a2 != a)
+			  {
+			    a->destroy();
+			    s.res_EventUniv->push_back(binop::instance(op,
+								       a2, b));
+			    result_ = recurse_destroy
+			      (multop::instance(multop::And, s.res_EventUniv));
+			    return;
+			  }
+			a2->destroy();
+			delete s.res_EventUniv;
+		      }
+		  if (op == binop::R || op == binop::M)
+		    if (const multop* mo = is_And(b))
+		      {
+			b->clone();
+			mospliter s(mospliter::Split_Univ, mo, c_);
+			const formula* b2 =
+			  multop::instance(multop::And, s.res_other);
+			if (b2 != b)
+			  {
+			    b->destroy();
+			    s.res_Univ->push_back(binop::instance(op, a, b2));
+			    result_ = recurse_destroy
+			      (multop::instance(multop::And, s.res_Univ));
+			    return;
+			  }
+			b2->destroy();
+			delete s.res_Univ;
+		      }
+		}
 
 	      trace << "bo: no eventuniv rule matched" << std::endl;
 	    }
@@ -2785,7 +3035,7 @@ namespace spot
 		    // Xa & Xb & FG(c) = X(a & b & FG(c))
 		    // For Universal&Eventual formulae f1...fn we also have:
 		    // Xa & Xb & f1...fn = X(a & b & f1...fn)
-		    if (!s.res_X->empty())
+		    if (!s.res_X->empty() && !opt_.favor_event_univ)
 		      {
 			s.res_X->push_back(allFG);
 			allFG = 0;
@@ -2794,13 +3044,49 @@ namespace spot
 					s.res_EventUniv->end());
 		      }
 		    else
-		      // We don't rewrite Ga & f1...fn = G(a & f1..fn)
-		      // similarly to what we do in the unop::Or case
-		      // as it is not clear what we'd gain by doing so.
+		      // If f1...fn are event&univ formulae, with at least
+		      // one formula of the form G(...),
+		      // Rewrite  g & f1...fn  as  g & G(f1..fn) while
+		      // stripping any leading G from f1...fn.
+		      // This gathers eventual&universal formulae
+		      // under the same term.
 		      {
-			s.res_other->insert(s.res_other->begin(),
-					    s.res_EventUniv->begin(),
-					    s.res_EventUniv->end());
+			multop::vec* eu = new multop::vec;
+			bool seen_g = false;
+			for (multop::vec::const_iterator
+			       i = s.res_EventUniv->begin();
+			     i != s.res_EventUniv->end(); ++i)
+			  {
+			    if ((*i)->is_eventual() && (*i)->is_universal())
+			      {
+				if (const unop* g = is_G(*i))
+				  {
+				    seen_g = true;
+				    eu->push_back(g->child()->clone());
+				    g->destroy();
+				  }
+				else
+				  {
+				    eu->push_back(*i);
+				  }
+			      }
+			    else
+			      s.res_other->push_back(*i);
+			  }
+			if (seen_g)
+			  {
+			    eu->push_back(allFG);
+			    allFG = 0;
+			    s.res_other->push_back(unop_multop(unop::G,
+							       multop::And,
+							       eu));
+			  }
+			else
+			  {
+			    s.res_other->insert(s.res_other->end(),
+						eu->begin(), eu->end());
+			    delete eu;
+			  }
 		      }
 		    delete s.res_EventUniv;
 
@@ -2964,7 +3250,7 @@ namespace spot
 		    //
 		    // In effect we rewrite
 		    //   Xa&Xb&GFc&GFd&Ge as X(a&b&G(Fc&Fd))&Ge
-		    if (!s.res_X->empty())
+		    if (!s.res_X->empty() && !opt_.favor_event_univ)
 		      {
 			multop::vec* event = new multop::vec;
 			for (multop::vec::iterator i = s.res_G->begin();
@@ -3511,7 +3797,7 @@ namespace spot
 		    // Xa | Xb | GF(c) = X(a | b | GF(c))
 		    // For Universal&Eventual formula f1...fn we also have:
 		    // Xa | Xb | f1...fn = X(a | b | f1...fn)
-		    if (!s.res_X->empty())
+		    if (!s.res_X->empty() && !opt_.favor_event_univ)
 		      {
 			s.res_X->push_back(allGF);
 			allGF = 0;
@@ -3519,7 +3805,8 @@ namespace spot
 					s.res_EventUniv->begin(),
 					s.res_EventUniv->end());
 		      }
-		    else if (!s.res_F->empty()
+		    else if (!opt_.favor_event_univ
+			     && !s.res_F->empty()
 			     && s.res_G->empty()
 			     && s.res_U_or_W->empty()
 			     && s.res_R_or_M->empty()
@@ -3538,7 +3825,7 @@ namespace spot
 			//   F(a|GFb)  3st.6tr. with initial self-loop
 			//   Fa|GFb    4st.8tr. without initial self-loop
 			//
-			// However, if other term are presents they will
+			// However, if other terms are presents they will
 			// prevent the formation of a self-loop, and the
 			// rewriting is unwelcome:
 			//   F(a|GFb)|Gc  5st.11tr.  without initial self-loop
@@ -3552,6 +3839,41 @@ namespace spot
 					s.res_EventUniv->begin(),
 					s.res_EventUniv->end());
 		      }
+		    else if (opt_.favor_event_univ)
+		      {
+			s.res_EventUniv->push_back(allGF);
+			allGF = 0;
+			bool seen_f = false;
+			if (s.res_EventUniv->size() > 1)
+			  {
+			    // If some of the EventUniv formulae start
+			    // with an F, Gather them all under the
+			    // same F.  Striping any leading F.
+			    for (multop::vec::iterator i =
+				   s.res_EventUniv->begin();
+				 i != s.res_EventUniv->end(); ++i)
+			      if (const unop* u = is_F(*i))
+				{
+				  *i = u->child()->clone();
+				  u->destroy();
+				  seen_f = true;
+				}
+			    if (seen_f)
+			      {
+				const formula* eu =
+				  unop_multop(unop::F, multop::Or,
+					      s.res_EventUniv);
+				s.res_EventUniv = 0;
+				s.res_other->push_back(eu);
+			      }
+			  }
+			if (!seen_f)
+			  {
+			    s.res_other->insert(s.res_other->end(),
+						s.res_EventUniv->begin(),
+						s.res_EventUniv->end());
+			  }
+		      }
 		    else
 		      {
 			s.res_other->insert(s.res_other->end(),
diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh
index 3f5133ea1..bed0d0630 100644
--- a/src/ltlvisit/simplify.hh
+++ b/src/ltlvisit/simplify.hh
@@ -38,7 +38,8 @@ namespace spot
 			     bool containment_checks_stronger = false,
 			     bool nenoform_stop_on_boolean = false,
 			     bool reduce_size_strictly = false,
-			     bool boolean_to_isop = false)
+			     bool boolean_to_isop = false,
+			     bool favor_event_univ = false)
 	: reduce_basics(basics),
 	  synt_impl(synt_impl),
 	  event_univ(event_univ),
@@ -46,7 +47,8 @@ namespace spot
 	  containment_checks_stronger(containment_checks_stronger),
 	  nenoform_stop_on_boolean(nenoform_stop_on_boolean),
 	  reduce_size_strictly(reduce_size_strictly),
-	  boolean_to_isop(boolean_to_isop)
+	  boolean_to_isop(boolean_to_isop),
+	  favor_event_univ(favor_event_univ)
       {
       }
 
@@ -64,6 +66,8 @@ namespace spot
       bool reduce_size_strictly;
       // If true, Boolean subformulae will be rewritten in ISOP form.
       bool boolean_to_isop;
+      // Try to isolate subformulae that are eventual and universal.
+      bool favor_event_univ;
     };
 
     // fwd declaration to hide technical details.
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index b109356a2..9e8ba524e 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -192,6 +192,8 @@ syntax(char* prog)
 	    << "  -rd   display the reduced formula" << std::endl
 	    << "  -rD   dump statistics about the simplifier cache" << std::endl
 	    << "  -rL   disable basic rewritings producing larger formulas"
+	    << std::endl
+	    << "  -ru   lift formulae that are eventual and universal"
 	    << std::endl << std::endl
 
 	    << "Automaton degeneralization (after translation):"
@@ -777,6 +779,12 @@ main(int argc, char** argv)
       else if (!strcmp(argv[formula_index], "-RT"))
         {
           opt_bisim_ta = true;
+	}
+      else if (!strcmp(argv[formula_index], "-ru"))
+        {
+	  simpltl = true;
+	  redopt.event_univ = true;
+	  redopt.favor_event_univ = true;
         }
       else if (!strcmp(argv[formula_index], "-M"))
         {
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index 8eb69f9a9..4ac82cf95 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -110,6 +110,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM) reduction7+ru of formula (pre reduction)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -r7 -ru -F -f -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction of formula in FM"
@@ -256,6 +264,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Compositional Suspension (-r4 -ru)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -u -r4 -ru -F -f -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM), degeneralized on states"