From 7fa19736136956cc3e0c9ca830e1750b740b832d Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Wed, 23 Oct 2024 14:00:15 +0200 Subject: [PATCH] expansions: fusion can produce false let's discard the result if it's false --- spot/tl/expansions.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index c09aec083..9978d925d 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -722,7 +722,10 @@ namespace spot if ((li & kj) != bddfalse) res.push_back({li & kj, fj}); } - res.push_back({li, formula::Fusion({ei, F})}); + + formula ei_fusion_F = formula::Fusion({ei, F}); + if (!ei_fusion_F.is(op::ff)) + res.push_back({li, ei_fusion_F}); } finalize(res, opts, d, seen);