simplify: add missing recursion

"1 U (a | Fb)" was not always reduced to "F(a | b)".

Fixes #143.

* spot/tl/simplify.cc: Add the missing recurse() call.
* tests/core/reduc0.test: Add a test.
* NEWS: Mention the bug.

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)
 

spot/tl/simplify.cc

 // -*- 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]))

tests/core/reduc0.test

 #! /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)'