diff --git a/NEWS b/NEWS
index 45e908127..76f850ac8 100644
--- a/NEWS
+++ b/NEWS
@@ -96,6 +96,9 @@ New in spot 2.8.5.dev (not yet released)
     spot.translate(..., 'det', 'any') triggered a syntax error in the
     Python code to handle this error.
 
+  - Some formulas with Boolean sub-formulas equivalent to true or
+    false could be translated into automata with false labels.
+
 New in spot 2.8.5 (2020-01-04)
 
   Bugs fixed:
diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc
index 3d09136bc..dcdc7feae 100644
--- a/spot/twaalgos/relabel.cc
+++ b/spot/twaalgos/relabel.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015-2018 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2015-2018, 2020 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -32,6 +32,7 @@ namespace spot
     std::set<int> newvars;
     vars.reserve(relmap->size());
     bool bool_subst = false;
+    bool need_cleanup = false;
 
     for (auto& p: *relmap)
       {
@@ -61,6 +62,8 @@ namespace spot
             bdd newb = formula_to_bdd(p.second, d, aut);
             bdd_setbddpair(pairs, oldv, newb);
             bool_subst = true;
+            if (newb == bddtrue || newb == bddfalse)
+              need_cleanup = true;
           }
       }
     if (!bool_subst)
@@ -76,5 +79,13 @@ namespace spot
     for (auto v: vars)
       if (newvars.find(v) == newvars.end())
         aut->unregister_ap(v);
+
+    // If some of the proposition are equivalent to true or false,
+    // it's possible that we have introduced edges with false labels.
+    if (need_cleanup)
+      {
+        aut->merge_edges();     // remove any edge labeled by 0
+        aut->purge_dead_states(); // remove useless states
+      }
   }
 }
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index 8bcf2bc71..603e7294c 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009-2019 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009-2020 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -431,3 +431,8 @@ cat >expected <<EOF
 8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1))
 8,(Fin(1) | Inf(0)) & (Fin(2) | Inf(1)) & (Fin(0) | Inf(2))
 EOF
+
+# This formula used to produce translation with false label.
+ltl2tgba -D -G 'F(G(a | !a) & ((b <-> c) W d))' | grep '\[f\]' && exit 1
+
+: