From c5746ef5cf1d9d939b5ddd1c987550c22c1c23df Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Thu, 13 Mar 2025 08:47:41 +0100 Subject: [PATCH] expansions: fix bogus false pairs in linear forms --- spot/tl/expansions2.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc index 96f970a94..c40298d7f 100644 --- a/spot/tl/expansions2.cc +++ b/spot/tl/expansions2.cc @@ -711,7 +711,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);