From f83a21cf942fc95c4297b559e6f4d6c829da0b49 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 13 Nov 2003 17:17:40 +0000
Subject: [PATCH] * src/tgbaalgos/emptinesscheck.cc
 (emptiness_check::complete_cycle): Check whether the state is in the current
 SCC before passing it to h_filt().

---
 ChangeLog                       | 6 ++++++
 src/tgbaalgos/emptinesscheck.cc | 8 ++++++--
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 1f58fc866..ead1aff22 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2003-11-13  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle):
+	Check whether the state is in the current SCC before passing it
+	to h_filt().
+
 2003-11-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::first_): New
diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc
index cb773cb2a..3bafbda19 100644
--- a/src/tgbaalgos/emptinesscheck.cc
+++ b/src/tgbaalgos/emptinesscheck.cc
@@ -425,11 +425,15 @@ namespace spot
 	todo.pop_front();
 	for (i->first(); !i->done(); i->next())
 	  {
-	    const state* dest = h_filt(i->current_state());
+	    const state* dest = i->current_state();
 
 	    // Do not escape this SCC.
 	    if (!scc.has_state(dest))
-	      continue;
+	      {
+		delete dest;
+		continue;
+	      }
+	    dest = h_filt(dest);
 
 	    bdd cond = i->current_condition();