From e663c222e564e516bc8d6f38da710e1ae7202169 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 21 Jan 2010 15:16:43 +0100
Subject: [PATCH] Fix taa_tgba_formula's destructor.

* src/tgba/taatgba.cc (taa_tgba_formula::~taa_tgba_formula):
Really destroy all formulae, not only half of them.
---
 ChangeLog           |  7 +++++++
 src/tgba/taatgba.cc | 11 +++++------
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 7d39e6bdb..189d6570c 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,10 @@
+2010-01-21  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Fix taa_tgba_formula's destructor.
+
+	* src/tgba/taatgba.cc (taa_tgba_formula::~taa_tgba_formula):
+	Really destroy all formulae, not only half of them.
+
 2010-01-21  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/tgbatest/randtgba.cc: Do not include <string> twice.
diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc
index 1b12d4993..97ccbe4d2 100644
--- a/src/tgba/taatgba.cc
+++ b/src/tgba/taatgba.cc
@@ -1,6 +1,5 @@
-// Copyright (C) 2009 Laboratoire d'Informatique de Paris
-// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-// Université Pierre et Marie Curie.
+// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -304,7 +303,7 @@ namespace spot
     }
     for (seen_map::iterator i = seen_.begin(); i != seen_.end();)
     {
-      // Advance the iterator before deleting the formula.
+      // Advance the iterator before deleting the state set.
       const spot::state_set* s = i->first;
       ++i;
       delete s;
@@ -386,12 +385,12 @@ namespace spot
   taa_tgba_formula::~taa_tgba_formula()
   {
     ns_map::iterator i;
-    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+    for (i = name_state_map_.begin(); i != name_state_map_.end();)
     {
       taa_tgba::state::iterator i2;
       for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
 	delete *i2;
-      // Advance the iterator before deleting the formula.
+      // Advance the iterator before destroying the formula.
       const ltl::formula* s = i->first;
       delete i->second;
       ++i;