diff --git a/NEWS b/NEWS
index 12b724fe0..da1c9f3d0 100644
--- a/NEWS
+++ b/NEWS
@@ -122,6 +122,9 @@ New in spot 2.8.7.dev (not yet released)
   - Emptiness checks, and scc_info should now ignore edges labeled
     with false.
 
+  - relabel_bse() could incorrectly relabel Boolean subformulas that
+    had some atomic propositions in common.
+
 New in spot 2.8.7 (2020-03-13)
 
   Bugs fixed:
diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc
index b594e4f1e..85273fa01 100644
--- a/spot/tl/relabel.cc
+++ b/spot/tl/relabel.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche et
+// Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -194,15 +194,15 @@ namespace spot
   //          ╱   ╲       ╱   ╲
   //         a─────b     c─────d
   //
-  // (The root node is also a cut-point, but we only consider Boolean
-  // cut-points for relabeling.)
+  // (The root node is also a cut point, but we only consider Boolean
+  // cut points for relabeling.)
   //
   // On the other hand, (a & b) U (b & !c) has only one Boolean
   // cut-point which corresponds to the NOT operator:
   //
   //             (a&b)U(b&!c)
   //                ╱   ╲
-  //              a&b   b&c
+  //              a&b   b&!c
   //             ╱   ╲ ╱   ╲
   //            a─────b────!c
   //                        │
@@ -222,7 +222,7 @@ namespace spot
   //     replace that node by a fresh atomic proposition.
   //
   // In the example above (a&b)U(b&!c), the last recursion
-  // stop a, b, and !c, producing (p0&p1)U(p1&p2).
+  // stops on a, b, and !c, producing (p0&p1)U(p1&p2).
   namespace
   {
     typedef std::vector<formula> succ_vec;
@@ -282,20 +282,23 @@ namespace spot
         if (sz > 1 && f.is_boolean())
           {
             // For Boolean nodes, connect all children in a
-            // loop.  This way the node can only be a cut-point
+            // loop.  This way the node can only be a cut point
             // if it separates all children from the reset of
             // the graph (not only one).
             formula pred = f[0];
             for (i = 1; i < sz; ++i)
               {
                 formula next = f[i];
-                // Note that we only add an edge in one
-                // direction, because we are building a cycle
-                // between all children anyway.
+                // Note that we only add an edge in both directions,
+                // as the cut point algorithm really need undirected
+                // graphs.  (We used to do only one direction, and
+                // that turned out to be a bug.)
                 g[pred].emplace_back(next);
+                g[next].emplace_back(pred);
                 pred = next;
               }
             g[pred].emplace_back(f[0]);
+            g[f[0]].emplace_back(pred);
           }
         s.pop();
       }
diff --git a/tests/core/ltlrel.test b/tests/core/ltlrel.test
index b734bee18..4449bd4f6 100755
--- a/tests/core/ltlrel.test
+++ b/tests/core/ltlrel.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2016 Laboratoire de Recherche et Développement
+# Copyright (C) 2013, 2016, 2020 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -89,3 +89,22 @@ Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & p3 & X((!p0 & p3) U p4)))) U p0)
   p3   ->   !p5
   p4   ->   p4
 EOF
+
+# The next two formulas come from a report by Jens Kreber.
+t <<EOF
+!b & e U (a & b & c)
+!p0 & (p1 U (p0 & p2 & p3))
+  p0   ->   b
+  p1   ->   e
+  p2   ->   a
+  p3   ->   c
+EOF
+t <<EOF
+X!c & X(b & c & d & a U e)
+X!p0 & X(p0 & p1 & p2 & (p3 U p4))
+  p0   ->   c
+  p1   ->   b
+  p2   ->   d
+  p3   ->   a
+  p4   ->   e
+EOF