diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 51a9b09a4..a0d2d6d97 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -935,6 +935,14 @@ namespace spot
 	      const formula* dest =
 		dict_.bdd_to_formula(bdd_exist(res & label, dict_.var_set));
 
+	      f2a_t::const_iterator i = f2a_.find(dest);
+	      if (i != f2a_.end() && i->second == 0)
+		{
+		  // This state is useless.  Ignore it.
+		  dest->destroy();
+		  continue;
+		}
+
 	      bool seen = a->has_state(dest);
 	      state_explicit_formula::transition* t =
 		a->create_transition(now, dest);
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index e6aefece9..3f29283ba 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -103,6 +103,10 @@ check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp;
 # before it is used in the translation.
 check_psl '{{b[*];c} | {{a && !a}}[=2]}'
 check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}'
+# When translating this formula, we expect the translator to ignore
+# `a;(f&!f)[=2];c' on one side because it as already seen it on the
+# other side.
+check_psl '{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c}'
 
 # Make sure 'a U (b U c)' has 3 states and 6 transitions,
 # before and after degeneralization.