diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc
index 42958fee5..43b7528f3 100644
--- a/iface/dve2/dve2.cc
+++ b/iface/dve2/dve2.cc
@@ -272,15 +272,17 @@ namespace spot
       }
 
       virtual
-      void first()
+      bool first()
       {
 	it_ = cc_->transitions.begin();
+	return it_ != cc_->transitions.end();
       }
 
       virtual
-      void next()
+      bool next()
       {
 	++it_;
+	return it_ != cc_->transitions.end();
       }
 
       virtual
diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc
index 0b8f5d6a9..990303a19 100644
--- a/src/kripke/kripkeexplicit.cc
+++ b/src/kripke/kripkeexplicit.cc
@@ -99,14 +99,16 @@ namespace spot
   {
   }
 
-  void kripke_explicit_succ_iterator::first()
+  bool kripke_explicit_succ_iterator::first()
   {
     it_ = s_->get_succ().begin();
+    return it_ != s_->get_succ().end();
   }
 
-  void kripke_explicit_succ_iterator::next()
+  bool kripke_explicit_succ_iterator::next()
   {
     ++it_;
+    return it_ != s_->get_succ().end();
   }
 
   bool kripke_explicit_succ_iterator::done() const
diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh
index c76f92a33..a2162d0e2 100644
--- a/src/kripke/kripkeexplicit.hh
+++ b/src/kripke/kripkeexplicit.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -97,8 +97,8 @@ namespace spot
 
     ~kripke_explicit_succ_iterator();
 
-    virtual void first();
-    virtual void next();
+    virtual bool first();
+    virtual bool next();
     virtual bool done() const;
 
     virtual state_kripke* current_state() const;
diff --git a/src/ta/ta.hh b/src/ta/ta.hh
index eebf71e84..a71b7d944 100644
--- a/src/ta/ta.hh
+++ b/src/ta/ta.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2013 Laboratoire de Recherche et
+// Copyright (C) 2010, 2012, 2013, 2014 Laboratoire de Recherche et
 // Developpement de l Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -191,12 +191,9 @@ namespace spot
     {
     }
 
-    virtual void
-    first() = 0;
-    virtual void
-    next() = 0;
-    virtual bool
-    done() const = 0;
+    virtual bool first() = 0;
+    virtual bool next() = 0;
+    virtual bool done() const = 0;
 
     virtual state*
     current_state() const = 0;
diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc
index b251bada5..407b87860 100644
--- a/src/ta/taexplicit.cc
+++ b/src/ta/taexplicit.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -54,24 +54,26 @@ namespace spot
     transitions_ = s->get_transitions(condition);
   }
 
-  void
+  bool
   ta_explicit_succ_iterator::first()
   {
-    if (transitions_ != 0)
-      i_ = transitions_->begin();
+    if (!transitions_)
+      return false;
+    i_ = transitions_->begin();
+    return i_ != transitions_->end();
   }
 
-  void
+  bool
   ta_explicit_succ_iterator::next()
   {
     ++i_;
+    return i_ != transitions_->end();
   }
 
   bool
   ta_explicit_succ_iterator::done() const
   {
-    return transitions_ == 0 || transitions_->empty() || i_
-        == transitions_->end();
+    return !transitions_ || i_ == transitions_->end();
   }
 
   state*
diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh
index 1be001caf..3cb0197aa 100644
--- a/src/ta/taexplicit.hh
+++ b/src/ta/taexplicit.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -248,12 +248,9 @@ namespace spot
 
     ta_explicit_succ_iterator(const state_ta_explicit* s, bdd condition);
 
-    virtual void
-    first();
-    virtual void
-    next();
-    virtual bool
-    done() const;
+    virtual bool first();
+    virtual bool next();
+    virtual bool done() const;
 
     virtual state*
     current_state() const;
diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc
index 9113ecd5d..f773ae68f 100644
--- a/src/ta/taproduct.cc
+++ b/src/ta/taproduct.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
+// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 //
@@ -150,17 +150,18 @@ namespace spot
 
   }
 
-  void
+  bool
   ta_succ_iterator_product::first()
   {
 
     next_kripke_dest();
 
     if (!done())
-      next_non_stuttering_();
+      return next_non_stuttering_();
+    return false;
   }
 
-  void
+  bool
   ta_succ_iterator_product::next()
   {
     delete current_state_;
@@ -173,11 +174,11 @@ namespace spot
       step_();
 
     if (!done())
-      next_non_stuttering_();
-
+      return next_non_stuttering_();
+    return false;
   }
 
-  void
+  bool
   ta_succ_iterator_product::next_non_stuttering_()
   {
 
@@ -190,7 +191,7 @@ namespace spot
             current_state_ = new state_ta_product(source_->get_ta_state(),
                 kripke_current_dest_state->clone());
             current_acceptance_conditions_ = bddfalse;
-            return;
+            return true;
           }
 
         if (!ta_succ_it_->done())
@@ -199,11 +200,12 @@ namespace spot
                 kripke_current_dest_state->clone());
             current_acceptance_conditions_
                 = ta_succ_it_->current_acceptance_conditions();
-            return;
+            return true;
           }
 
         step_();
       }
+    return false;
   }
 
   bool
diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh
index aabf9a90e..300f0dd2b 100644
--- a/src/ta/taproduct.hh
+++ b/src/ta/taproduct.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -83,12 +83,9 @@ namespace spot
     ~ta_succ_iterator_product();
 
     // iteration
-    void
-    first();
-    void
-    next();
-    bool
-    done() const;
+    bool first();
+    bool next();
+    bool done() const;
 
     // inspection
     state_ta_product*
@@ -106,10 +103,8 @@ namespace spot
   protected:
     //@{
     /// Internal routines to advance to the next successor.
-    void
-    step_();
-    void
-    next_non_stuttering_();
+    void step_();
+    bool next_non_stuttering_();
 
     /// \brief Move to the next successor in the kripke structure
     void
diff --git a/src/ta/tgtaproduct.cc b/src/ta/tgtaproduct.cc
index 2466fe3c0..b11f7c6f3 100644
--- a/src/ta/tgtaproduct.cc
+++ b/src/ta/tgtaproduct.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012 Laboratoire de Recherche et Developpement
+// Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement
 // de l Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -173,19 +173,16 @@ namespace spot
 
   }
 
-  void
+  bool
   tgta_succ_iterator_product::first()
   {
 
     next_kripke_dest();
-    trace
-      << "*** first() .... if(done()) = ***" << done() << std::endl;
-    if (!done())
-      find_next_succ_();
-
+    trace << "*** first() .... if(done()) = ***" << done() << std::endl;
+    return find_next_succ_();
   }
 
-  void
+  bool
   tgta_succ_iterator_product::next()
   {
     current_state_->destroy();
@@ -193,18 +190,14 @@ namespace spot
 
     step_();
 
-    trace
-      << "*** next() .... if(done()) = ***" << done() << std::endl;
-
-    if (!done())
-      find_next_succ_();
+    trace << "*** next() .... if(done()) = ***" << done() << std::endl;
 
+    return find_next_succ_();
   }
 
-  void
+  bool
   tgta_succ_iterator_product::find_next_succ_()
   {
-
     while (!done())
       {
         if (!tgta_succ_it_->done())
@@ -214,11 +207,12 @@ namespace spot
                 tgta_succ_it_->current_state(), pool_);
             current_acceptance_conditions_
                 = tgta_succ_it_->current_acceptance_conditions();
-            return;
+            return true;
           }
 
         step_();
       }
+    return false;
   }
 
   bool
diff --git a/src/ta/tgtaproduct.hh b/src/ta/tgtaproduct.hh
index 58aa364af..955797026 100644
--- a/src/ta/tgtaproduct.hh
+++ b/src/ta/tgtaproduct.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -54,12 +54,9 @@ namespace spot
     ~tgta_succ_iterator_product();
 
     // iteration
-    void
-    first();
-    void
-    next();
-    bool
-    done() const;
+    bool first();
+    bool next();
+    bool done() const;
 
     // inspection
     state_product*
@@ -75,8 +72,7 @@ namespace spot
     /// Internal routines to advance to the next successor.
     void
     step_();
-    void
-    find_next_succ_();
+    bool find_next_succ_();
 
     void
     next_kripke_dest();
diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh
index 94030f295..ce8574f8d 100644
--- a/src/tgba/succiter.hh
+++ b/src/tgba/succiter.hh
@@ -53,17 +53,21 @@ namespace spot
     /// This method can be called several times to make multiple
     /// passes over successors.
     ///
-    /// \warning One should always call \c done() to
-    /// ensure there is a successor, even after \c first().  A
-    /// common trap is to assume that there is at least one
-    /// successor: this is wrong.
-    virtual void first() = 0;
+    /// \warning One should always call \c done() (or better: check
+    /// the return value of first()) to ensure there is a successor,
+    /// even after \c first().  A common trap is to assume that there
+    /// is at least one successor: this is wrong.
+    ///
+    /// \return whether there is actually a successor
+    virtual bool first() = 0;
 
     /// \brief Jump to the next successor (if any).
     ///
-    /// \warning Again, one should always call \c done() to ensure
-    /// there is a successor.
-    virtual void next() = 0;
+    /// \warning Again, one should always call \c done() (or better:
+    /// check the return value of next()) ensure there is a successor.
+    ///
+    /// \return whether there is actually a successor
+    virtual bool next() = 0;
 
     /// \brief Check whether the iteration is finished.
     ///
@@ -132,8 +136,7 @@ namespace spot
 
       void operator++()
       {
-	it_->next();
-	if (it_->done())
+	if (!it_->next())
 	  it_ = nullptr;
       }
     };
diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc
index 58b4b84f0..bd5df3bc0 100644
--- a/src/tgba/succiterconcrete.cc
+++ b/src/tgba/succiterconcrete.cc
@@ -29,16 +29,18 @@ namespace spot
   {
   }
 
-  void
+  bool
   tgba_succ_iterator_concrete::first()
   {
     succ_set_left_ = succ_set_;
     current_ = bddfalse;
     if (!done())
-      next();
+      return next();
+    else
+      return false;
   }
 
-  void
+  bool
   tgba_succ_iterator_concrete::next()
   {
     assert(!done());
@@ -86,7 +88,7 @@ namespace spot
 
 	succ_set_left_ -= current_;
 	if (succ_set_left_ == bddfalse) // No more successors?
-	  return;
+	  return false;
 
 	// Pick one transition, and extract its destination.
 	bdd trans = bdd_satoneset(succ_set_left_, data_.next_set,
@@ -157,6 +159,8 @@ namespace spot
 	current_state_ = bdd_replace(dest, data_.dict->next_to_now);
       }
     while ((current_state_ & data_.relation) == bddfalse);
+
+    return succ_set_left_ != bddfalse;
   }
 
   bool
diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh
index f69bd6d35..b9eebbc75 100644
--- a/src/tgba/succiterconcrete.hh
+++ b/src/tgba/succiterconcrete.hh
@@ -61,8 +61,8 @@ namespace spot
     virtual ~tgba_succ_iterator_concrete();
 
     // iteration
-    void first();
-    void next();
+    bool first();
+    bool next();
     bool done() const;
 
     // inspection
diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc
index 1e60bca84..7dde18c1c 100644
--- a/src/tgba/taatgba.cc
+++ b/src/tgba/taatgba.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE)
+// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -315,16 +315,18 @@ namespace spot
     }
   }
 
-  void
+  bool
   taa_succ_iterator::first()
   {
     i_ = succ_.begin();
+    return i_ != succ_.end();
   }
 
-  void
+  bool
   taa_succ_iterator::next()
   {
     ++i_;
+    return i_ != succ_.end();
   }
 
   bool
diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh
index 66dbeb464..4e5e08d11 100644
--- a/src/tgba/taatgba.hh
+++ b/src/tgba/taatgba.hh
@@ -113,8 +113,8 @@ namespace spot
     taa_succ_iterator(const taa_tgba::state_set* s, bdd all_acc);
     virtual ~taa_succ_iterator();
 
-    virtual void first();
-    virtual void next();
+    virtual bool first();
+    virtual bool next();
     virtual bool done() const;
 
     virtual set_state* current_state() const;
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index b419382a1..3c68652ed 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -102,8 +102,7 @@ namespace spot
 
       internal::succ_iterator begin()
       {
-	it_->first();
-	return it_->done() ? nullptr : it_;
+	return it_->first() ? it_ : nullptr;
       }
 
       internal::succ_iterator end()
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index bfa82230b..1eadd08eb 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -208,14 +208,16 @@ namespace spot
       all_acceptance_conditions_ = all_acc;
     }
 
-    virtual void first()
+    virtual bool first()
     {
       it_ = start_->successors.begin();
+      return it_ != start_->successors.end();
     }
 
-    virtual void next()
+    virtual bool next()
     {
       ++it_;
+      return it_ != start_->successors.end();
     }
 
     virtual bool done() const
diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc
index b8b5cfd22..8e18897e9 100644
--- a/src/tgba/tgbakvcomplement.cc
+++ b/src/tgba/tgbakvcomplement.cc
@@ -258,8 +258,8 @@ namespace spot
 				       const state_kv_complement* origin);
       virtual ~tgba_kv_complement_succ_iterator() {};
 
-      virtual void first();
-      virtual void next();
+      virtual bool first();
+      virtual bool next();
       virtual bool done() const;
       virtual state_kv_complement* current_state() const;
       virtual bdd current_condition() const;
@@ -470,24 +470,25 @@ namespace spot
       current_ranks_ = highest_current_ranks_;
     }
 
-    void
+    bool
     tgba_kv_complement_succ_iterator::first()
     {
       current_condition_ = condition_list_.begin();
-      if (done())
-        return;
+      if (current_condition_ == condition_list_.end())
+        return false;
 
       successor_highest_rank(*current_condition_);
 
       if (!is_valid_rank())
         next_valid_rank();
+      return current_condition_ != condition_list_.end();
     }
 
-    void
+    bool
     tgba_kv_complement_succ_iterator::next()
     {
-      if (done())
-        return;
+      if (current_condition_ == condition_list_.end())
+        return false;
 
       if (!next_valid_rank())
       {
@@ -499,12 +500,13 @@ namespace spot
             next_valid_rank();
         }
       }
+      return current_condition_ != condition_list_.end();
     }
 
     bool
     tgba_kv_complement_succ_iterator::done() const
     {
-      return (current_condition_ == condition_list_.end());
+      return current_condition_ == condition_list_.end();
     }
 
     state_kv_complement*
diff --git a/src/tgba/tgbamask.cc b/src/tgba/tgbamask.cc
index 23bfc24f8..8557bbc14 100644
--- a/src/tgba/tgbamask.cc
+++ b/src/tgba/tgbamask.cc
@@ -40,14 +40,16 @@ namespace spot
 	  t.dest->destroy();
       }
 
-      void first()
+      bool first()
       {
 	it_ = trans_.begin();
+	return it_ != trans_.end();
       }
 
-      virtual void next()
+      bool next()
       {
 	++it_;
+	return it_ != trans_.end();
       }
 
       bool done() const
diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc
index 073a792be..896570b6e 100644
--- a/src/tgba/tgbaproduct.cc
+++ b/src/tgba/tgbaproduct.cc
@@ -104,26 +104,24 @@ namespace spot
 	delete right_;
       }
 
-      virtual void next_non_false_() = 0;
+      virtual bool next_non_false_() = 0;
 
-    void first()
+      bool first()
       {
 	if (!right_)
-	  return;
+	  return false;
 
-	left_->first();
-	right_->first();
 	// If one of the two successor sets is empty initially, we
 	// reset right_, so that done() can detect this situation
 	// easily.  (We choose to reset right_ because this variable
 	// is already used by done().)
-	if (left_->done() || right_->done())
+	if (!(left_->first() && right_->first()))
 	  {
 	    delete right_;
 	    right_ = 0;
-	    return;
+	    return false;
 	  }
-	next_non_false_();
+	return next_non_false_();
       }
 
       bool done() const
@@ -166,19 +164,18 @@ namespace spot
       {
       }
 
-      void step_()
+      bool step_()
       {
-	left_->next();
-	if (left_->done())
-	  {
-	    left_->first();
-	    right_->next();
-	  }
+	if (left_->next())
+	  return true;
+	left_->first();
+	return right_->next();
       }
 
-      void next_non_false_()
+      bool next_non_false_()
       {
-	while (!done())
+	assert(!done());
+	do
 	  {
 	    bdd l = left_->current_condition();
 	    bdd r = right_->current_condition();
@@ -187,16 +184,18 @@ namespace spot
 	    if (current_cond != bddfalse)
 	      {
 		current_cond_ = current_cond;
-		return;
+		return true;
 	      }
-	    step_();
 	  }
+	while (step_());
+	return false;
       }
 
-      void next()
+      bool next()
       {
-	step_();
-	next_non_false_();
+	if (step_())
+	  return next_non_false_();
+	return false;
       }
 
       bdd current_condition() const
@@ -235,12 +234,13 @@ namespace spot
       {
       }
 
-      void next_non_false_()
+      bool next_non_false_()
       {
 	// All the transitions of left_ iterator have the
 	// same label, because it is a Kripke structure.
 	bdd l = left_->current_condition();
-	while (!right_->done())
+	assert(!right_->done());
+	do
 	  {
 	    bdd r = right_->current_condition();
 	    bdd current_cond = l & r;
@@ -248,21 +248,21 @@ namespace spot
 	    if (current_cond != bddfalse)
 	      {
 		current_cond_ = current_cond;
-		return;
+		return true;
 	      }
-	    right_->next();
 	  }
+	while (right_->next());
+	return false;
       }
 
-      void next()
+      bool next()
       {
-	left_->next();
-	if (left_->done())
-	  {
-	    left_->first();
-	    right_->next();
-	    next_non_false_();
-	  }
+	if (left_->next())
+	  return true;
+	left_->first();
+	if (right_->next())
+	  return next_non_false_();
+	return false;
       }
 
       bdd current_condition() const
diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc
index 68d29fc80..9655650aa 100644
--- a/src/tgba/tgbasafracomplement.cc
+++ b/src/tgba/tgbasafracomplement.cc
@@ -976,8 +976,8 @@ namespace spot
           delete p.second;
       }
 
-      virtual void first();
-      virtual void next();
+      virtual bool first();
+      virtual bool next();
       virtual bool done() const;
       virtual state_complement* current_state() const;
       virtual bdd current_condition() const;
@@ -988,16 +988,18 @@ namespace spot
       succ_list_t::const_iterator it_;
     };
 
-    void
+    bool
     tgba_safra_complement_succ_iterator::first()
     {
       it_ = list_.begin();
+      return it_ != list_.end();
     }
 
-    void
+    bool
     tgba_safra_complement_succ_iterator::next()
     {
       ++it_;
+      return it_ != list_.end();
     }
 
     bool
diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc
index 763311bb6..c5b876906 100644
--- a/src/tgba/tgbasgba.cc
+++ b/src/tgba/tgbasgba.cc
@@ -1,5 +1,6 @@
-// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2011, 2012, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -113,16 +114,16 @@ namespace spot
 
       // iteration
 
-      void
+      bool
       first()
       {
-	it_->first();
+	return it_->first();
       }
 
-      void
+      bool
       next()
       {
-	it_->next();
+	return it_->next();
       }
 
       bool
diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc
index 89660b031..803ba77d2 100644
--- a/src/tgba/tgbatba.cc
+++ b/src/tgba/tgbatba.cc
@@ -348,16 +348,18 @@ namespace spot
 
       // iteration
 
-      void
+      bool
       first()
       {
 	it_ = translist_.begin();
+	return it_ != translist_.end();
       }
 
-      void
+      bool
       next()
       {
 	++it_;
+	return it_ != translist_.end();
       }
 
       bool
diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc
index a8cf690c9..d727de92a 100644
--- a/src/tgba/tgbaunion.cc
+++ b/src/tgba/tgbaunion.cc
@@ -111,62 +111,94 @@ namespace spot
     delete right_;
   }
 
-  void
+  bool
   tgba_succ_iterator_union::next()
   {
     // Is it the initial state ?
     if (left_ && right_)
-    {
-      // Yes, first iterate on the successors of the initial state of the
-      // left automaton.
-      if (!left_->done())
       {
-	left_->next();
+	// Yes, first iterate on the successors of the initial state of the
+	// left automaton.
 	if (!left_->done())
-	  current_cond_ = left_->current_condition();
+	  {
+	    if (left_->next())
+	      {
+		current_cond_ = left_->current_condition();
+		return true;
+	      }
+	    else if (!right_->done())
+	      {
+		current_cond_ = right_->current_condition();
+		return true;
+	      }
+	    else
+	      {
+		return false;
+	      }
+	  }
+	// Now iterate with the successors of the initial state of the right
+	// automaton.
 	else
-	  current_cond_ = right_->current_condition();
+	  {
+	    if (right_->next())
+	      {
+		current_cond_ = right_->current_condition();
+		return true;
+	      }
+	    else
+	      {
+		return false;
+	      }
+	  }
       }
-      // Now iterate with the successors of the initial state of the right
-      // automaton.
-      else
-      {
-	right_->next();
-	if (!right_->done())
-	  current_cond_ = right_->current_condition();
-      }
-    }
     else
-    {
-      // No, iterate either on the left or the right automaton.
-      if (left_)
       {
-	left_->next();
-	if (!left_->done())
-	  current_cond_ = left_->current_condition();
+	// No, iterate either on the left or the right automaton.
+	if (left_)
+	  {
+	    if (left_->next())
+	      {
+		current_cond_ = left_->current_condition();
+		return true;
+	      }
+	    else
+	      {
+		return false;
+	      }
+	  }
+	else
+	  {
+	    if (right_->next())
+	      {
+		current_cond_ = right_->current_condition();
+		return true;
+	      }
+	    else
+	      {
+		return false;
+	      }
+	  }
       }
-      else
-      {
-	right_->next();
-	if (!right_->done())
-	  current_cond_ = right_->current_condition();
-      }
-    }
   }
 
-  void
+  bool
   tgba_succ_iterator_union::first()
   {
+    bool r = false;
     if (right_)
-    {
-      right_->first();
-      current_cond_ = right_->current_condition();
-    }
+      {
+	r = right_->first();
+	if (r)
+	  current_cond_ = right_->current_condition();
+      }
+    bool l = false;
     if (left_)
-    {
-      left_->first();
-      current_cond_ = left_->current_condition();
-    }
+      {
+	l = left_->first();
+	if (l)
+	  current_cond_ = left_->current_condition();
+      }
+    return r || l;
   }
 
   bool
diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh
index 3e9a5f15c..b520da5bd 100644
--- a/src/tgba/tgbaunion.hh
+++ b/src/tgba/tgbaunion.hh
@@ -90,8 +90,8 @@ namespace spot
     virtual ~tgba_succ_iterator_union();
 
     // iteration
-    void first();
-    void next();
+    bool first();
+    bool next();
     bool done() const;
 
     // inspection
diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc
index 30c54dc48..7a23d363c 100644
--- a/src/tgba/wdbacomp.cc
+++ b/src/tgba/wdbacomp.cc
@@ -109,20 +109,32 @@ namespace spot
 
       // iteration
 
-      void
+      bool
       first()
       {
+	left_ = bddtrue;
 	if (it_)
 	  it_->first();
-	left_ = bddtrue;
+	// Return true even if it_ is done, because
+	// we have to build a sink state.
+	return true;
       }
 
-      void
+      bool
       next()
       {
-	left_ -= current_condition();
-	if (it_)
-	  it_->next();
+	if (!it_ || it_->done())
+	  {
+	    left_ = bddfalse;
+	    return false;
+	  }
+	left_ -= it_->current_condition();
+	if (left_ == bddfalse)
+	  return false;
+	it_->next();
+	// Return true even if it_ is done, because
+	// we have to build a sink state.
+	return true;
       }
 
       bool