diff --git a/ChangeLog b/ChangeLog
index 27bdd8e41..5cf219b2d 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,24 @@
+2010-03-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Optimize tgba_tba_proxy and tgba_sba_proxy for states that share
+	an acceptance condition on all outgoing transitions.
+
+	This was motivated by experiments from Rüdiger Ehlers, showing
+	that "ltl2ba -f 'a U (b U c)'" outperformed "ltl2tgba -f -N -R3 'a
+	U (b U c)'".  With this change and the previous one, it is no
+	longer the case.
+
+	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::aut_): Store
+	a pointer to the source automaton and...
+	(tgba_tba_proxy_succ_iterator::sync_): ... use it in an extra
+	optimization step to gather the acceptance conditions common
+	to all outgoing transitions of the destination state, and pretend
+	they are on the current (ingoing) transition.
+	(tgba_tba_proxy::succ_iter): Pass the
+	source automaton to the constructed iterator.
+	* src/tgbatest/spotlbtt.test: Test -f -N -R3 -r7.
+	* src/tgbatest/ltl2tgba.test: Add a test case for 'a U (b U c)'.
+
 2010-03-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	ltl2tgba: apply -R3 before -D or -DS.
diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc
index 575b3731d..a17bdd867 100644
--- a/src/tgba/tgbatba.cc
+++ b/src/tgba/tgbatba.cc
@@ -1,6 +1,8 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// l'Epita.
+// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -114,9 +116,10 @@ namespace spot
       tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it,
 				   iterator expected,
 				   const list& cycle,
-				   bdd the_acceptance_cond)
+				   bdd the_acceptance_cond,
+				   const tgba* aut)
 	: it_(it), expected_(expected), cycle_(cycle),
-	  the_acceptance_cond_(the_acceptance_cond)
+	  the_acceptance_cond_(the_acceptance_cond), aut_(aut)
       {
       }
 
@@ -203,6 +206,20 @@ namespace spot
 	    //   month	= {December}
 	    // }
 
+
+	    // As an extra optimization step, gather the acceptance
+	    // conditions common to all outgoing transitions of the
+	    // destination state, and pretend they are already present
+	    // on this transition.
+	    bdd common = aut_->all_acceptance_conditions();
+	    state* dest = it_->current_state();
+	    tgba_succ_iterator* dest_it = aut_->succ_iter(dest);
+	    for (dest_it->first(); !dest_it->done(); dest_it->next())
+	      common &= dest_it->current_acceptance_conditions();
+	    acc |= common;
+	    delete dest_it;
+	    delete dest;
+
 	    next_ = expected_;
 	    while (next_ != cycle_.end() && (acc & *next_) == *next_)
 	      ++next_;
@@ -226,6 +243,7 @@ namespace spot
       bool accepting_;
       const list& cycle_;
       const bdd the_acceptance_cond_;
+      const tgba* aut_;
       friend class ::spot::tgba_tba_proxy;
     };
 
@@ -281,7 +299,8 @@ namespace spot
 					   global_state, global_automaton);
 
     return new tgba_tba_proxy_succ_iterator(it, s->acceptance_iterator(),
-					    acc_cycle_, the_acceptance_cond_);
+					    acc_cycle_, the_acceptance_cond_,
+					    a_);
   }
 
   bdd_dict*
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index fa2341bfb..3be074a71 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -50,3 +50,12 @@ check 'a R (b R c)'
 check '(a U b) U (c U d)'
 
 check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
+
+
+# Make sure 'a U (b U c)' has 3 states and 6 transitions,
+# before and after degeneralization.
+for opt in '' -D -DS; do
+  ../ltl2tgba -k -f -R3 $opt 'a U (b U c)' > stdout
+  grep 'transitions: 6$' stdout
+  grep 'states: 3$' stdout
+done
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index b0b926d72..829f3946f 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -270,6 +270,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), pre + post reduction, via never claim"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spin '../ltl2tgba -F -f -N -R3 -r7'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Tauriainen -- TAA)"