From 98f67973ebb5b0a134cde42296c5b3db25715071 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 7 Nov 2011 10:03:50 +0100
Subject: [PATCH] Speedup minimize_obligation() when
 f->is_syntactic_obligation().

* src/tgbaalgos/minimize.cc (minimize_obligation): Do not check
the output of minimize_wdba if the input formula is a syntactic
obligation.
---
 src/tgbaalgos/minimize.cc | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc
index e74a944c9..35e97d9e5 100644
--- a/src/tgbaalgos/minimize.cc
+++ b/src/tgbaalgos/minimize.cc
@@ -625,12 +625,15 @@ namespace spot
   {
     tgba_explicit_number* min_aut_f = minimize_wdba(aut_f);
 
+    // if f is a syntactic obligation formula, the WDBA minimization
+    // must be correct.
+    if (f && f->is_syntactic_obligation())
+      return min_aut_f;
+
     // If aut_f is a guarantee automaton, the WDBA minimization must be
     // correct.
     if (is_guarantee_automaton(aut_f))
-      {
-	return min_aut_f;
-      }
+      return min_aut_f;
 
     if (!f && !aut_neg_f)
       {