diff --git a/NEWS b/NEWS
index 7d026bea7..b481495e0 100644
--- a/NEWS
+++ b/NEWS
@@ -14,9 +14,11 @@ New in spot 1.2.3a (not yet released)
     - "ltl2tgta --ta" could crash in certain conditions due to the
       introduction of a simulation-based reduction after
       degeneralization.
-    - Fix three incorrect simplifications rules, all related to the
-      factorization of Boolean subformulas in operands of the
-      non-length-matching "&" SERE operator.
+    - Fix four incorrect formula-simplification rules, three were
+      related to the factorization of Boolean subformulas in
+      operands of the non-length-matching "&" SERE operator, and
+      a fourth one could only be enabled by explicitely passing the
+      favor_event_univ option to the simplifier (not the default).
     - Fix incorrect translation of the fusion operator (":") in SERE
       such as {xx;1}:yy[*] where the left operand has 1 as tail.
 
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 18d89f1f8..b843ff41e 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1580,7 +1580,6 @@ $q,\,q_i$           & a pure eventuality that is also purely universal \\
               &                     & 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*}
diff --git a/src/ltltest/eventuniv.test b/src/ltltest/eventuniv.test
index 195322795..304e3c903 100755
--- a/src/ltltest/eventuniv.test
+++ b/src/ltltest/eventuniv.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
-# de l'Epita (LRDE).
+# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+# Developpement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -48,7 +48,7 @@ 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) W g'  '(a | Gc) W g'   # Unchanged
 check '(a | Gc) U g'  '(a | Gc) U g'   # Unchanged
 
 check '(a & GFc) M b' '(a M b) & GFc'
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index c2ce125d7..88c93c5be 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -2075,7 +2075,6 @@ namespace spot
 	      // (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)
@@ -2099,24 +2098,6 @@ namespace spot
 			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))
 		      {