diff --git a/ChangeLog b/ChangeLog
index db2a7ce03..137cffe36 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,20 @@
+2011-12-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Perform WDBA minimization before degeneralization.
+
+	There is no point in degeneralizing an automaton if it can be WDBA
+	minimized.  Doing so will only augment the number of states and
+	slow down the powerset construction used by the WDBA minimization.
+
+	* src/tgbatest/babiak.test: New file.  It includes 5 formulae
+	which Tomáš Babiak reported Spot 0.7.1 would take over one hour to
+	translate if degeneralization and WDBA minimization were both
+	requested.
+	* src/tgbatest/Makefile.am (TESTS): Add it.
+	* src/tgbatest/ltl2tgba.cc: Do WDBA minimization before
+	degeneralization.  The above formulae are now all translated in a
+	few seconds.
+
 2011-12-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Don't rely on the g++ version to include tr1/unordered_map and co.
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index a0e69af54..f2fd0c53f 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -100,6 +100,7 @@ TESTS = \
   sccsimpl.test \
   obligation.test \
   wdba.test \
+  babiak.test \
   randtgba.test \
   emptchk.test \
   emptchke.test \
diff --git a/src/tgbatest/babiak.test b/src/tgbatest/babiak.test
new file mode 100755
index 000000000..ca2501412
--- /dev/null
+++ b/src/tgbatest/babiak.test
@@ -0,0 +1,115 @@
+#!/bin/sh
+# Copyright (C) 2011 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+# While running some benchmark, Tomáš Babiak found that Spot took too
+# much time (i.e. >1h) to translate those six formulae.  It turns out
+# that the WDBA minimization was performed after the degeneralization
+# algorithm, while this is not necessary (WDBA will produce a BA, so
+# we may as well skip degeneralization).  Translating these formulae
+# in the test-suite ensure that they don't take too much time (the
+# buildfarm will timeout if it does).
+
+. ./defs
+
+set -e
+
+cat >formulae <<EOF
+(p6 V X(G(F(F(X X(F X(F((G X F p1)|((F p5)U p1))))U((F p4)&(!p2|(G p0))))))))
+(F((G 1)&(!p6 V X!p2)))V((F((G X(!p1 V!p3))V F!p2))U(X((G p3)U(p6 U p7))V X p5))
+(((F p0)V((F p3)&!p4))V((((!p0|!p5)V X!p5)V p6)U(p5|(!p3 U(G(p1 U p2))))))
+(G(((F((p3 &!p3)|(G((G!p2)V!p5))))|(p1 V!p4))U((X(G((F!p0)U!p6))U X!p2)|!p7)))
+X((X(!p1 V F!p6)V F!p4)U p2)&(F(G((0 U(F p6))U((p1 U(G(p4 U F p0)))U X p7))))
+(G(G(((F p5)U((((F!p1)V(p2 &!p4))|!p2)|((X!p7 U!p4)V(F(F((G p2)&p5))))))U p6)))
+EOF
+
+cat > config <<EOF
+Algorithm
+{
+   Name = "Spot/FM basic"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -F -f -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot/FM, with reductions + degeneralization (neverclaim)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spin '../ltl2tgba -r4 -R3f -F -f -N'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot/FM, with reducetion + WDBA + degeneralization (neverclaim)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spin '../ltl2tgba -r7 -R3 -f -x -N -F -Rm'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot/FM, with reducetion + WDBA + degeneralization (DS)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -r7 -R3 -f -x -DS -t -F -Rm'"
+   Enabled = yes
+}
+
+GlobalOptions
+{
+   Rounds = 6
+   Interactive = Never
+#   Verbosity = 5
+#   ComparisonCheck = no
+#   ConsistencyCheck = no
+#   IntersectionCheck = no
+}
+
+# Not used, but LBTT seems to want it.
+FormulaOptions
+{
+  Size = 1...13
+  Propositions = 6
+
+  AbbreviatedOperators = Yes
+  GenerateMode = Normal
+  OutputMode = Normal
+  PropositionPriority = 50
+
+  TruePriority = 1
+  FalsePriority = 1
+
+  AndPriority = 10
+  OrPriority = 10
+  XorPriority = 0
+  # EquivalencePriority = 0
+
+  BeforePriority = 0
+
+  DefaultOperatorPriority = 5
+}
+EOF
+
+${LBTT} --formulafile=formulae
+rm config
+
+
+
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 05311c6af..6fc076151 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -934,27 +934,6 @@ main(int argc, char** argv)
       const spot::tgba_tba_proxy* degeneralized = 0;
       const spot::tgba_sgba_proxy* state_labeled = 0;
 
-      unsigned int n_acc = a->number_of_acceptance_conditions();
-      if (echeck_inst
-	  && degeneralize_opt == NoDegen
-	  && n_acc > 1
-	  && echeck_inst->max_acceptance_conditions() < n_acc)
-	degeneralize_opt = DegenTBA;
-
-      if (degeneralize_opt == DegenTBA)
-	{
-	  a = degeneralized = new spot::tgba_tba_proxy(a);
-	}
-      else if (degeneralize_opt == DegenSBA)
-	{
-	  a = degeneralized = new spot::tgba_sba_proxy(a);
-	  assume_sba = true;
-	}
-      else if (labeling_opt == StateLabeled)
-	{
-	  a = state_labeled = new spot::tgba_sgba_proxy(a);
-	}
-
       const spot::tgba* minimized = 0;
       if (opt_minimize)
 	{
@@ -983,6 +962,33 @@ main(int argc, char** argv)
 	    }
 	}
 
+      unsigned int n_acc = a->number_of_acceptance_conditions();
+      if (echeck_inst
+	  && degeneralize_opt == NoDegen
+	  && n_acc > 1
+	  && echeck_inst->max_acceptance_conditions() < n_acc)
+	{
+	  degeneralize_opt = DegenTBA;
+	  assume_sba = false;
+	}
+
+      if (!assume_sba && !opt_monitor)
+	{
+	  if (degeneralize_opt == DegenTBA)
+	    {
+	      a = degeneralized = new spot::tgba_tba_proxy(a);
+	    }
+	  else if (degeneralize_opt == DegenSBA)
+	    {
+	      a = degeneralized = new spot::tgba_sba_proxy(a);
+	      assume_sba = true;
+	    }
+	  else if (labeling_opt == StateLabeled)
+	    {
+	      a = state_labeled = new spot::tgba_sgba_proxy(a);
+	    }
+	}
+
       if (opt_monitor)
 	{
 	  tm.start("Monitor minimization");