diff --git a/ChangeLog b/ChangeLog
index 2a1db273f..31ba83365 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,17 @@
+2004-05-10  Thomas MARTINEZ  <martinez@abacus.lip6.fr>
+
+	* src/ltltest/formules.ltl: A pattern of 2000 formulas.
+	* src/ltltest/inf.test: Test some case of implies.
+	* src/ltltest/inf.cc: Test some case of implies.
+	* src/ltltest/reduc.test: Test reduction of a file of formula.
+	* src/ltltest/reduc.cc: Test reduction of a formula.
+
+	* src/ltlvisit/formlength.cc: Gives the lenght of a formula.
+	* src/ltlvisit/forminf.cc: To know if a formula implies an other.
+	* src/ltlvisit/basereduc.cc: Implement only basic reduction.
+	* src/ltlvisit/reducform.cc: Implement reduction.
+	* src/ltlvisit/reducform.hh: To reduce a formula.
+
 2004-05-10  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Refine
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index d2020eec1..663d3773b 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -24,6 +24,7 @@
 #include <fstream>
 #include <string>
 #include "ltlvisit/destroy.hh"
+#include "ltlvisit/reducform.hh"
 #include "ltlast/allnodes.hh"
 #include "ltlparse/public.hh"
 #include "tgbaalgos/ltl2tgba_lacim.hh"
@@ -91,7 +92,9 @@ syntax(char* prog)
 	    << "  -X   do not compute an automaton, read it from a file"
 	    << std::endl
 	    << "  -y   do not merge states with same symbolic representation "
-	    << "(implies -f)" << std::endl;
+	    << "(implies -f)" << std::endl
+	    << "  -z   to reduce formula "
+	    << std::endl;
   exit(2);
 }
 
@@ -113,6 +116,7 @@ main(int argc, char** argv)
   bool magic_many = false;
   bool expect_counter_example = false;
   bool from_file = false;
+  bool reduc = false;
   bool post_branching = false;
   bool fair_loop_approx = false;
 
@@ -250,6 +254,10 @@ main(int argc, char** argv)
 	  fm_opt = true;
 	  fm_symb_merge_opt = false;
 	}
+      else if (!strcmp(argv[formula_index], "-z"))
+	{
+	  reduc = true;
+	}
       else
 	{
 	  break;
@@ -312,6 +320,9 @@ main(int argc, char** argv)
 	}
       else
 	{
+	  spot::ltl::formula* ftmp = f;
+	  if (reduc)
+	    f = spot::ltl::reduce(f);
 	  if (fm_opt)
 	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
 					       fm_symb_merge_opt,
@@ -319,6 +330,11 @@ main(int argc, char** argv)
 					       fair_loop_approx);
 	  else
 	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
+
+	  if (reduc)
+	    spot::ltl::destroy(ftmp);
+	  spot::ltl::destroy(f);
+
 	}
 
       spot::tgba_tba_proxy* degeneralized = 0;