From 983d7e046a9aada23ba49c8ca7ed6dfabbb613f4 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Thu, 13 Mar 2025 08:47:41 +0100 Subject: [PATCH 1/2] expansions: remove unused lambda capture --- spot/tl/expansions2.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc index d80e5ffa3..96f970a94 100644 --- a/spot/tl/expansions2.cc +++ b/spot/tl/expansions2.cc @@ -540,7 +540,7 @@ namespace spot return {{f_bdd, formula::eword()}}; } - auto rec = [&d, owner, opts, seen](formula f){ + auto rec = [&d, owner, seen](formula f){ return expansion2(f, d, owner, exp_opts::None, seen); }; From 8e9f4dc12d8fa0c79302238cd91d896eff10d4ce Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Thu, 13 Mar 2025 08:47:41 +0100 Subject: [PATCH 2/2] 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);