diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 6899adbf8..b7e3e13a8 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -266,8 +266,14 @@ namespace spot scc_info si(susp_aut, scc_info_options::NONE); if (si.is_trivial(si.scc_of(susp_aut->get_init_state_number()))) { - assert(!si.is_trivial(0)); - susp_aut->set_init_state(si.one_state_of(0)); + unsigned st = si.one_state_of(0); + // The bottom SCC can actually be trivial if it + // has no successor because the formula is + // equivalent to false. + assert(!si.is_trivial(0) || + susp_aut->out(st).begin() + == susp_aut->out(st).end()); + susp_aut->set_init_state(st); susp_aut->purge_unreachable_states(); } } diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index fcd004f6e..588e7b57e 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -364,12 +364,14 @@ diff output expected # The first four formulas appear in a NEWS entry for Spot 2.6 # The 5th one is from issue #267. +# The 6th one is from issue #358. cat >formulas <