From eeaed5592f06007aa57f54f6c6632b91b392d01c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 8 Dec 2020 11:56:29 +0100
Subject: [PATCH] fix ignored aborter in WDBA-minimization

Fixes #443, reported by Roei Nahum.  (However the fix
only works for the development version, where wdba-det-max
was introduced to work around that kind of problem.)

* spot/twaalgos/minimize.cc: Avoid aborter being implicitly
converted to Boolean.
* tests/core/ltl2tgba2.test: Add test case.
* THANKS: Add Roei Nahum.
---
 THANKS                    | 1 +
 spot/twaalgos/minimize.cc | 3 +--
 tests/core/ltl2tgba2.test | 4 ++++
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/THANKS b/THANKS
index 090f09bae..7d3596140 100644
--- a/THANKS
+++ b/THANKS
@@ -40,6 +40,7 @@ Ming-Hsien Tsai
 Nikos Gorogiannis
 Paul Guénézan
 Reuben Rowe
+Roei Nahum
 Rüdiger Ehlers
 Silien Hong
 Simon Jantsch
diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 49d7b7864..be603c7f1 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -386,7 +386,6 @@ namespace spot
     twa_graph_ptr det_a;
 
     {
-      power_map pm;
       bool input_is_det = is_deterministic(a);
       if (input_is_det)
         {
@@ -394,7 +393,7 @@ namespace spot
         }
       else
         {
-          det_a = tgba_powerset(a, pm, aborter);
+          det_a = tgba_powerset(a, aborter);
           if (!det_a)
             return nullptr;
         }
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index 2887c8bec..c8f53c53c 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -474,3 +474,7 @@ test "4,1" = `ltl2tgba -D --med "$f" --stats=%s,%d`
 # Issue #418.
 f='(G!a | G!b | G!c) & (FG!a2 | GFb2 | GFc2) & (GFc2 | FG!b2 | GFa2)'
 test 28 = `ltl2tgba -D -G -S --stats=%s "$f"`
+
+# Issue #443.  This used to be too long.
+f='(!(G({(a)} |=> {(b)[*32]})))'
+test 34 = `ltl2tgba -B --stats=%s "$f"`