diff --git a/ChangeLog b/ChangeLog index 643459091..7882812f0 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2004-05-14 Alexandre Duret-Lutz + * src/tgbaalgos/gtec/gtec.cc (emptiness_check::remove_component): + Do not try to erase state that are not found in H. + Report from Soheib Baarir. + * src/ltltest/reduc.test: Use ./defs and clean result.data. * src/ltltest/Makefile.am (CLEANFILES): Clean result.data. diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 1d8b147a0..1582f809c 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -64,7 +64,15 @@ namespace spot { state* s = i->current_state(); numbered_state_heap::state_index_p spi = ecs_->h->index(s); - assert(spi.second); + + // This state is not necessary in H, because if we were + // doing inclusion checking during the emptiness-check + // (redefining find()), the index `s' can be included in a + // larger state and will not be found by index(). We can + // safely ignore such states. + if (!spi.first) + continue; + if (*spi.second != -1) { *spi.second = -1;