From a0cd56735a6ba732b07995557d55d062589adb89 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 14 Jun 2016 09:56:17 +0200
Subject: [PATCH] relabel: fix infinite recursion in relabel_bse()
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reported by František Blahoudek.

* spot/tl/relabel.cc: Fix.
* tests/core/ltlrel.test: Add test case.
* NEWS: Mention the bug.
---
 NEWS                   |  1 +
 spot/tl/relabel.cc     |  3 ++-
 tests/core/ltlrel.test | 14 +++++++++++++-
 3 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index ed6ef44bf..1f540d30e 100644
--- a/NEWS
+++ b/NEWS
@@ -79,6 +79,7 @@ New in spot 2.0.1a (not yet released)
 
   * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1
     headers.
+  * Fix an infinite recursion in relabel_bse().
 
 New in spot 2.0.1 (2016-05-09)
 
diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc
index 05270453e..90e2a6f0a 100644
--- a/spot/tl/relabel.cc
+++ b/spot/tl/relabel.cc
@@ -433,13 +433,14 @@ namespace spot
         /// it as ((a & b) & Xc) in the graph to isolate the
         /// Boolean operands as a single node.
         formula b = f.boolean_operands(&i);
-        if (b)
+        if (b && b != f)
           {
             res.reserve(sz - i + 1);
             res.push_back(visit(b));
           }
         else
           {
+            i = 0;
             res.reserve(sz);
           }
         for (; i < sz; ++i)
diff --git a/tests/core/ltlrel.test b/tests/core/ltlrel.test
index 13c4de3a0..4f403ef66 100755
--- a/tests/core/ltlrel.test
+++ b/tests/core/ltlrel.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et Dévelopement to
+# Copyright (C) 2013, 2016 Laboratoire de Recherche et Dévelopement to
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -77,3 +77,15 @@ t <<EOF
   p1   ->   b
   p2   ->   c
 EOF
+
+# This one used to stack overflow due to an infinite recursion
+# in the relabeling function.  Reported by František Blahoudek.
+t <<EOF
+<>p1 -> ((p0 -> (!p1 U (!p1 && p3 && !p5 && X((!p1 && !p5) U p4)))) U p1)
+Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & p3 & X((!p0 & p3) U p4)))) U p0)
+  p0   ->   p1
+  p1   ->   p0
+  p2   ->   p3
+  p3   ->   !p5
+  p4   ->   p4
+EOF