From 4e1c8dfd74c25e82be8803943f23c049210934f0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 19 Nov 2016 14:49:46 +0100 Subject: [PATCH] add test-case for bdd_noderesize MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * tests/core/ltl2tgba.test: Add new test-case, reported by Tomáš Babiak. * NEWS: Mention the bug fixed by previous patch. --- NEWS | 4 +++- tests/core/ltl2tgba.test | 6 ++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 70bd50da4..80a5b63cb 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 2.2.0.dev (not yet released) - Nothing yet. + Bugs: + + * The bdd_noderesize() function, as modified in 2.2, would crash. New in spot 2.2 (2016-11-14) diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index c907c15d8..bdfbd0805 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -224,3 +224,9 @@ grep 'ltl2tgba: unknown option.*@' stderr # Make sure the count of AP is correct through never claims or LBTT ltl2tgba -f a -s | autfilt -q --ap=1 --lbtt | autfilt -q --ap=1 + +# Such a large formula will fill the BuDDy unicity table and trigger a +# resize. At the time this test is introduced, this is the only place +# of the test-suite where this resize is triggered, so do not remove +# it unless you can find another place that triggers that. +genltl --go-theta=18 | ltl2tgba --low --any -q