From f0735d4d86a593335ab4f08c05f5f3b7a607dd39 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 11 Nov 2017 08:59:01 +0100
Subject: [PATCH] wdba_minimization: avoid translating !f when input is
 deterministic

* spot/twaalgos/minimize.cc (wdba_minimization): Here.
---
 spot/twaalgos/minimize.cc | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 86200e37c..a78cbc876 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -619,7 +619,13 @@ namespace spot
     // Build negation automaton if not supplied.
     if (!aut_neg_f)
       {
-        if (f)
+        if (is_deterministic(aut_f))
+          {
+            // If the automaton is deterministic, complementing is
+            // easy.
+            aut_neg_f = remove_fin(dualize(aut_f));
+          }
+        else if (f)
           {
             // If we know the formula, simply build the automaton for
             // its negation.
@@ -627,12 +633,6 @@ namespace spot
             // Remove useless SCCs.
             aut_neg_f = scc_filter(aut_neg_f, true);
           }
-        else if (is_deterministic(aut_f))
-          {
-            // If the automaton is deterministic, complementing is
-            // easy.
-            aut_neg_f = remove_fin(dualize(aut_f));
-          }
         else
           {
             // Otherwise, we cannot check if the minimization is safe.