diff --git a/NEWS b/NEWS
index 930eb576d..89a650120 100644
--- a/NEWS
+++ b/NEWS
@@ -63,6 +63,7 @@ New in spot 1.99.7a (not yet released)
     (regression introduced in 1.99.7)
   * ltlfilt, autfilt, randltl, and randaut could easily crash when
     compiled statically (i.e., with configure --disable-shared).
+  * "1 U (a | Fb)" was not always simplified to "F(a | b)".
 
 New in spot 1.99.7 (2016-01-15)
 
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 1605647fb..2de13b385 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
-// et Developpement de l'Epita (LRDE).
+// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de
+// Recherche et Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -1645,7 +1645,7 @@ namespace spot
 		  return b;
 		// if !a => b, then a U b = Fb
 		if (c_->implication_neg(a, b, false))
-		  return formula::F(b);
+		  return recurse(formula::F(b));
 		// if a => b, then a U (b U c) = (b U c)
 		// if a => b, then a U (b W c) = (b W c)
 		if (b.is(op::U, op::W) && c_->implication(a, b[0]))
diff --git a/tests/core/reduc0.test b/tests/core/reduc0.test
index dd3a06787..99a89195c 100755
--- a/tests/core/reduc0.test
+++ b/tests/core/reduc0.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -35,3 +35,6 @@ run 0 ../reduc 0 '!{a[*];{b && !b}}'
 # Triggered an assert  before
 run 0 ../reduc 0 '(a | (Xa M a))'
 run 0 ../reduc 0 '(b xor (Xb U b)) <-> e'
+
+
+run 0 ../reduc 3 '1 U (a | Fb)' 'F(a | b)'