diff --git a/ChangeLog b/ChangeLog
index 3fc8177de..511ea8c89 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2010-01-20  Damien Lefortier <dam@lrde.epita.fr>
+
+	When iterating a hash_map, be careful not to delete i->first
+	before doing ++i to avoid memory issues.
+
+	* src/tgba/taatgba.cc, src/tgba/taatgba.hh,
+	src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Fix them.
+
 2010-01-20  Damien Lefortier <dam@lrde.epita.fr>
 
 	Minor fixes to compile with GCC 3.3
diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc
index 8e5afbdde..1b12d4993 100644
--- a/src/tgba/taatgba.cc
+++ b/src/tgba/taatgba.cc
@@ -302,8 +302,13 @@ namespace spot
       delete succ_[i]->dst;
       delete succ_[i];
     }
-    for (seen_map::iterator i = seen_.begin(); i != seen_.end(); ++i)
-      delete i->first;
+    for (seen_map::iterator i = seen_.begin(); i != seen_.end();)
+    {
+      // Advance the iterator before deleting the formula.
+      const spot::state_set* s = i->first;
+      ++i;
+      delete s;
+    }
   }
 
   void
@@ -350,6 +355,18 @@ namespace spot
   | taa_tgba_string |
   `----------------*/
 
+  taa_tgba_string::~taa_tgba_string()
+  {
+    ns_map::iterator i;
+    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+    {
+      taa_tgba::state::iterator i2;
+      for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	delete *i2;
+      delete i->second;
+    }
+  }
+
   std::string
   taa_tgba_string::label_to_string(const label_t& label) const
   {
@@ -370,7 +387,16 @@ namespace spot
   {
     ns_map::iterator i;
     for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-      i->first->destroy();
+    {
+      taa_tgba::state::iterator i2;
+      for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	delete *i2;
+      // Advance the iterator before deleting the formula.
+      const ltl::formula* s = i->first;
+      delete i->second;
+      ++i;
+      s->destroy();
+    }
   }
 
   std::string
diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh
index afd5cc328..ff188b654 100644
--- a/src/tgba/taatgba.hh
+++ b/src/tgba/taatgba.hh
@@ -159,18 +159,6 @@ namespace spot
   public:
     taa_tgba_labelled(bdd_dict* dict) : taa_tgba(dict) {};
 
-    virtual ~taa_tgba_labelled()
-    {
-      typename ns_map::iterator i;
-      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-      {
-	taa_tgba::state::iterator i2;
-	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
-	  delete *i2;
-	delete i->second;
-      }
-    }
-
     void set_init_state(const label& s)
     {
       std::vector<label> v(1);
@@ -344,6 +332,7 @@ namespace spot
   public:
     taa_tgba_string(bdd_dict* dict) :
       taa_tgba_labelled<std::string, string_hash>(dict) {};
+    ~taa_tgba_string();
   protected:
     virtual std::string label_to_string(const std::string& label) const;
     virtual std::string clone_if(const std::string& label) const;
@@ -355,7 +344,6 @@ namespace spot
   public:
     taa_tgba_formula(bdd_dict* dict) :
       taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict) {};
-    // Labels are pointers here and must be destroyed eventually.
     ~taa_tgba_formula();
   protected:
     virtual std::string label_to_string(const label_t& label) const;
diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc
index 4d572adcf..06e697621 100644
--- a/src/tgba/tgbaexplicit.cc
+++ b/src/tgba/tgbaexplicit.cc
@@ -284,6 +284,18 @@ namespace spot
     return neg_acceptance_conditions_;
   }
 
+  tgba_explicit_string::~tgba_explicit_string()
+  {
+    ns_map::iterator i;
+    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+    {
+      tgba_explicit::state::iterator i2;
+      for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	delete *i2;
+      delete i->second;
+    }
+  }
+
   tgba_explicit::state*
   tgba_explicit_string::add_default_init()
   {
@@ -302,9 +314,18 @@ namespace spot
 
   tgba_explicit_formula::~tgba_explicit_formula()
   {
-    ns_map::iterator i;
-    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-      i->first->destroy();
+    ns_map::iterator i = name_state_map_.begin();
+    while (i != name_state_map_.end())
+    {
+      tgba_explicit::state::iterator i2;
+      for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	delete *i2;
+      // Advance the iterator before deleting the formula.
+      const ltl::formula* s = i->first;
+      delete i->second;
+      ++i;
+      s->destroy();
+    }
   }
 
   tgba_explicit::state* tgba_explicit_formula::add_default_init()
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index 202441744..e81e4340c 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -142,11 +142,6 @@ namespace spot
   public:
     tgba_explicit_succ_iterator(const tgba_explicit::state* s, bdd all_acc);
 
-    virtual
-    ~tgba_explicit_succ_iterator()
-    {
-    }
-
     virtual void first();
     virtual void next();
     virtual bool done() const;
@@ -312,14 +307,6 @@ namespace spot
     virtual
     ~tgba_explicit_labelled()
     {
-      typename ns_map::iterator i;
-      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-	{
-	  tgba_explicit::state::iterator i2;
-	  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
-	    delete *i2;
-	  delete i->second;
-	}
     }
 
   };
@@ -331,6 +318,7 @@ namespace spot
     tgba_explicit_string(bdd_dict* dict):
       tgba_explicit_labelled<std::string, string_hash>(dict)
     {};
+    virtual ~tgba_explicit_string();
     virtual state* add_default_init();
     virtual std::string format_state(const spot::state* s) const;
   };