alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

relabel: fix infinite recursion in relabel_bse()

Browse source 
Reported by František Blahoudek.

* spot/tl/relabel.cc: Fix.
* tests/core/ltlrel.test: Add test case.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2016-06-14 09:56:17 +02:00
parent 272daf62fc
commit a0cd56735a
3 changed files with 16 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
spot/tl/relabel.cc
View file

@ -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)