diff --git a/ChangeLog b/ChangeLog
index 53335cd9f..07de7ba26 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2004-05-17  Thomas Martinez  <martinez@src.lip6.fr>
+
+	* src/ltlvisit/basereduc.cc (spot): 80 columns.
+	* src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc,
+	src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh,
+	src/tgbatest/ltl2tgba.cc (main): More option.
+	* src/ltltest/inf.test: More test.
+
 2004-05-17  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* wrap/python/buddy.i: Define typemap for input_buf and use it
diff --git a/src/ltltest/inf.cc b/src/ltltest/inf.cc
index 375d249f3..935389b64 100644
--- a/src/ltltest/inf.cc
+++ b/src/ltltest/inf.cc
@@ -41,21 +41,22 @@ syntax(char* prog)
 int
 main(int argc, char** argv)
 {
-  if (argc < 3)
+  if (argc < 4)
     syntax(argv[0]);
 
+  int opt = atoi(argv[1]);
 
   spot::ltl::parse_error_list p1;
-  spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+  spot::ltl::formula* f1 = spot::ltl::parse(argv[2], p1);
   spot::ltl::formula* f2 = NULL;
 
-  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
+  if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
     return 2;
 
   spot::ltl::parse_error_list p2;
-  f2 = spot::ltl::parse(argv[2], p2);
+  f2 = spot::ltl::parse(argv[3], p2);
 
-  if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
+  if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
     return 2;
 
   std::string f1s = spot::ltl::to_string(f1);
@@ -63,28 +64,36 @@ main(int argc, char** argv)
 
   int exit_return = 0;
 
-  std::cout << "Test f1 < f2" << std::endl;
-  if (spot::ltl::inf_form(f1, f2))
+  switch (opt)
     {
-      std::cout << f1s << " < " << f2s << std::endl;
-      exit_return = 1;
-    }
+    case 0:
+      std::cout << "Test f1 < f2" << std::endl;
+      if (spot::ltl::inf_form(f1, f2))
+	{
+	  std::cout << f1s << " < " << f2s << std::endl;
+	  exit_return = 1;
+	}
+      break;
 
-  /*
-  std::cout << "Test !f1 < f2" << std::endl;
-  if (spot::ltl::infneg_form(f1, f2, 0))
-    {
-      std::cout << "!(" << f1s << ") < " << f2s << std::endl;
-      exit_return = 2;
-    }
+    case 1:
+      std::cout << "Test !f1 < f2" << std::endl;
+      if (spot::ltl::infneg_form(f1, f2, 0))
+	{
+	  std::cout << "!(" << f1s << ") < " << f2s << std::endl;
+	  exit_return = 1;
+	}
+      break;
 
-  std::cout << "Test f1 < !f2" << std::endl;
-  if (spot::ltl::infneg_form(f1, f2, 1))
-    {
-      std::cout << f1s << " < !(" << f2s << ")" << std::endl;
-      exit_return = 3;
+    case 2:
+      std::cout << "Test f1 < !f2" << std::endl;
+      if (spot::ltl::infneg_form(f1, f2, 1))
+	{
+	  std::cout << f1s << " < !(" << f2s << ")" << std::endl;
+	  exit_return = 1;
+	}
+      break;
+    default: break;
     }
-  */
 
   spot::ltl::dump(std::cout, f1); std::cout << std::endl;
   spot::ltl::dump(std::cout, f2); std::cout << std::endl;
diff --git a/src/ltltest/inf.test b/src/ltltest/inf.test
index d01dd6449..824166835 100755
--- a/src/ltltest/inf.test
+++ b/src/ltltest/inf.test
@@ -26,67 +26,67 @@
 . ./defs || exit 1
 
 #
-run 1 ./inf 'Xa' 'X(b U a)'
-run 1 ./inf 'XXa' 'XX(b U a)'
+run 1 ./inf 0 'Xa' 'X(b U a)'
+run 1 ./inf 0 'XXa' 'XX(b U a)'
 
-run 1 ./inf '(e R f)' '(g U f)'
-run 1 ./inf '( X(a + b))' '( X((a + b)+(c)+(d)))'
-run 1 ./inf '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
+run 1 ./inf 0 '(e R f)' '(g U f)'
+run 1 ./inf 0 '( X(a + b))' '( X((a + b)+(c)+(d)))'
+run 1 ./inf 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
 
-run 0 ./inf 'Xa' 'XX(b U a)'
-run 0 ./inf 'XXa' 'X(b U a)'
+run 0 ./inf 0 'Xa' 'XX(b U a)'
+run 0 ./inf 0 'XXa' 'X(b U a)'
 
-run 0 ./inf '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
-run 0 ./inf '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
+run 0 ./inf 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
+run 0 ./inf 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
 
-run 0 ./inf 'a' 'b'
-run 0 ./inf 'a' 'b + c'
-run 0 ./inf 'a + b' 'a'
-run 0 ./inf 'a' 'a * c'
-run 0 ./inf 'a * b' 'c'
-run 0 ./inf 'a' 'a U b'
-run 0 ./inf 'a' 'a R b'
-run 0 ./inf 'a R b' 'a'
+run 0 ./inf 0 'a' 'b'
+run 0 ./inf 0 'a' 'b + c'
+run 0 ./inf 0 'a + b' 'a'
+run 0 ./inf 0 'a' 'a * c'
+run 0 ./inf 0 'a * b' 'c'
+run 0 ./inf 0 'a' 'a U b'
+run 0 ./inf 0 'a' 'a R b'
+run 0 ./inf 0 'a R b' 'a'
 
-run 1 ./inf '1' '1'
-run 1 ./inf '0' '0'
+run 1 ./inf 0 '1' '1'
+run 1 ./inf 0 '0' '0'
 
-run 1 ./inf 'a' '1'
-run 1 ./inf 'a' 'a'
+run 1 ./inf 0 'a' '1'
+run 1 ./inf 0 'a' 'a'
 
-run 1 ./inf 'a' 'a * 1'
+run 1 ./inf 0 'a' 'a * 1'
 
-run 1 ./inf 'a * b' 'b'
-run 1 ./inf 'a * b' 'a'
+run 1 ./inf 0 'a * b' 'b'
+run 1 ./inf 0 'a * b' 'a'
 
-run 1 ./inf 'a' 'a + b'
-run 1 ./inf 'b' 'a + b'
+run 1 ./inf 0 'a' 'a + b'
+run 1 ./inf 0 'b' 'a + b'
 
-run 1 ./inf 'a + b' '1'
+run 1 ./inf 0 'a + b' '1'
 
-run 1 ./inf 'a' 'b U a'
-run 1 ./inf 'a' 'b U 1'
-run 1 ./inf 'a U b' '1'
+run 1 ./inf 0 'a' 'b U a'
+run 1 ./inf 0 'a' 'b U 1'
+run 1 ./inf 0 'a U b' '1'
 
-run 1 ./inf 'a' '1 R a'
-run 1 ./inf 'a' 'a R 1'
-run 1 ./inf 'a R b' 'b'
-run 1 ./inf 'a R b' '1'
+run 1 ./inf 0 'a' '1 R a'
+run 1 ./inf 0 'a' 'a R 1'
+run 1 ./inf 0 'a R b' 'b'
+run 1 ./inf 0 'a R b' '1'
 
-run 1 ./inf 'Xa' 'X(b U a)'
-run 1 ./inf 'X(a R b)' 'Xb'
+run 1 ./inf 0 'Xa' 'X(b U a)'
+run 1 ./inf 0 'X(a R b)' 'Xb'
 
-run 1 ./inf 'a U b' '1 U b'
-run 1 ./inf 'a R b' '1 R b'
+run 1 ./inf 0 'a U b' '1 U b'
+run 1 ./inf 0 'a R b' '1 R b'
 
-run 1 ./inf 'b * (a U b)' 'a U b'
-run 1 ./inf 'a U b' 'c + (a U b)'
+run 1 ./inf 0 'b * (a U b)' 'a U b'
+run 1 ./inf 0 'a U b' 'c + (a U b)'
 
 exit 0
 #
 
-#run 1 ./inf '(a U b) U ((a U b) U (a U b))' 'a U b'
-#run 1 ./inf '(a U b) && (a U b)' 'a U b'
+#run 1 ./inf 0 '(a U b) U ((a U b) U (a U b))' 'a U b'
+#run 1 ./inf 0 '(a U b) && (a U b)' 'a U b'
 
 'X1' '1'
 'a U 0' '0'
diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc
index 582581ad4..f4a9dbc3d 100644
--- a/src/ltltest/reduc.cc
+++ b/src/ltltest/reduc.cc
@@ -59,6 +59,15 @@ main(int argc, char** argv)
     case 3:
       o = spot::ltl::BRI;
       break;
+    case 4:
+      o = spot::ltl::InfBase;
+      break;
+    case 5:
+      o = spot::ltl::EventualUniversalBase;
+      break;
+    case 6:
+      o = spot::ltl::InfEventualUniversal;
+      break;
     default:
       return 2;
   }
diff --git a/src/ltlvisit/basereduc.cc b/src/ltlvisit/basereduc.cc
index 2b3eb54ce..d1f8a7a24 100644
--- a/src/ltlvisit/basereduc.cc
+++ b/src/ltlvisit/basereduc.cc
@@ -70,6 +70,9 @@ namespace spot
       {
 	formula* f = uo->child();
 	result_ = basic_reduce_form(f);
+	multop* mo = NULL;
+	unop* u = NULL;
+	binop* bo = NULL;
 	switch (uo->op())
 	  {
 	  case unop::Not:
@@ -87,30 +90,31 @@ namespace spot
 
 	    /* X(f1 & GF(f2)) = X(f1) & GF(F2) */
 	    /* X(f1 | GF(f2)) = X(f1) | GF(F2) */
-	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
-	      if (dynamic_cast<multop*>(result_)->size() == 2) {
-		if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
-		  //|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
+	    mo = dynamic_cast<multop*>(result_);
+	    if (mo && mo->size() == 2)
+	      {
+		if (is_GF(mo->nth(0)))
+		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
-		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
-		    f = result_;
-		    result_ = multop::instance(dynamic_cast<multop*>(result_)->op(), res);
-		    spot::ltl::destroy(f);
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce_form(mo->nth(1))));
+		    res->push_back(basic_reduce_form(mo->nth(0)));
+		    result_ = multop::instance(mo->op(), res);
+		    spot::ltl::destroy(mo);
 		    return;
 		  }
-		if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
-		  //|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
+		if (is_GF(mo->nth(1)))
+		  {
 		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
-		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
-		    f = result_;
-		    result_ = multop::instance(dynamic_cast<multop*>(result_)->op(), res);
-		    spot::ltl::destroy(f);
+		    res->push_back(unop::instance(unop::F,
+						  basic_reduce_form(mo->nth(0))));
+		    res->push_back(basic_reduce_form(mo->nth(1)));
+		    result_ = multop::instance(mo->op(), res);
+		    spot::ltl::destroy(mo);
 		    return;
 		  }
-		}
-	    }
+	      }
+
 
 	    result_ = unop::instance(unop::X, result_);
 	    return;
@@ -123,41 +127,46 @@ namespace spot
 	      return;
 
 	    /* FX(a) = XF(a) */
-	    if (node_type(result_) == (node_type_form_visitor::Unop))
-	      if (dynamic_cast<unop*>(result_)->op() == unop::X){
-		f = result_;
-		result_ = unop::instance(unop::X,
-					 unop::instance(unop::F,
-							basic_reduce_form(dynamic_cast<unop*>(result_)->child()) ));
-		spot::ltl::destroy(f);
-		return;
-	      }
+	    u = dynamic_cast<unop*>(result_);
+	    if (u && u->op() == unop::X)
+	      {
+		result_ =
+		  unop::instance(unop::X,
+				 unop::instance(unop::F,
+						basic_reduce_form(u->child())));
+		spot::ltl::destroy(u);
+	      return;
+	    }
 
 	    /* F(f1 & GF(f2)) = F(f1) & GF(F2) */
-	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
-	      if (dynamic_cast<multop*>(result_)->op() == multop::And) {
-		if (dynamic_cast<multop*>(result_)->size() == 2) {
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
-		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
-		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
-		    spot::ltl::destroy(result_);
-		    result_ = multop::instance(multop::And, res);
-		    return;
+	    mo = dynamic_cast<multop*>(result_);
+	    if (mo && mo->op() == multop::And)
+	      {
+		if (mo->size() == 2)
+		  {
+		    if (is_GF(mo->nth(0)))
+		      {
+			multop::vec* res = new multop::vec;
+			res->push_back(unop::instance(unop::F,
+						      basic_reduce_form(mo->nth(1))));
+			res->push_back(basic_reduce_form(mo->nth(0)));
+			result_ = multop::instance(mo->op(), res);
+			spot::ltl::destroy(mo);
+			return;
+		      }
+		    if (is_GF(mo->nth(1)))
+		      {
+			multop::vec* res = new multop::vec;
+			res->push_back(unop::instance(unop::F,
+						      basic_reduce_form(mo->nth(0))));
+			res->push_back(basic_reduce_form(mo->nth(1)));
+			result_ = multop::instance(mo->op(), res);
+			spot::ltl::destroy(mo);
+			return;
+		      }
 		  }
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
-		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::F, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
-		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
-		    spot::ltl::destroy(result_);
-		    result_ = multop::instance(multop::And, res);
-		    return;
-		  }
-		}
 	      }
-	    }
+
 
 	    result_ = unop::instance(unop::F, result_);
 	    return;
@@ -170,50 +179,56 @@ namespace spot
 	      return;
 
 	    /* G(a R b) = G(b) */
-	    if (node_type(result_) == node_type_form_visitor::Binop)
-	      if (dynamic_cast<binop*>(result_)->op() == binop::R){
-		f = result_;
-		result_ = unop::instance(unop::G, basic_reduce_form(dynamic_cast<binop*>(result_)->second()));
-		spot::ltl::destroy(f);
+	    bo = dynamic_cast<binop*>(result_);
+	    if (bo && bo->op() == binop::R)
+	      {
+		result_ = unop::instance(unop::G,
+					 basic_reduce_form(bo->second()));
+		spot::ltl::destroy(bo);
 		return;
 	      }
 
 	    /* GX(a) = XG(a) */
-	    if (node_type(result_) == (node_type_form_visitor::Unop))
-	      if ( dynamic_cast<unop*>(result_)->op() == unop::X ){
-		f = result_;
-		result_ = unop::instance(unop::X,
-					 unop::instance(unop::G,
-							basic_reduce_form(dynamic_cast<unop*>(result_)->child())));
-		spot::ltl::destroy(f);
+	    u = dynamic_cast<unop*>(result_);
+	    if (u && u->op() == unop::X)
+	      {
+		result_ =
+		  unop::instance(unop::X,
+				 unop::instance(unop::G,
+						basic_reduce_form(u->child())));
+		spot::ltl::destroy(u);
 		return;
 	      }
 
 	    /* G(f1 | GF(f2)) = G(f1) | GF(F2) */
-	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
-	      if (dynamic_cast<multop*>(f)->op() == multop::Or) {
-		if (dynamic_cast<multop*>(result_)->size() == 2) {
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(0))) {
-		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(0))) {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1))));
-		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0)));
-		    spot::ltl::destroy(result_);
-		    result_ = multop::instance(multop::Or, res);
-		    return;
+	    mo = dynamic_cast<multop*>(result_);
+	    if (mo && mo->op() == multop::Or)
+	      {
+		if (mo->size() == 2)
+		  {
+		    if (is_GF(mo->nth(0)))
+		      {
+			multop::vec* res = new multop::vec;
+			res->push_back(unop::instance(unop::F,
+						      basic_reduce_form(mo->nth(1))));
+			res->push_back(basic_reduce_form(mo->nth(0)));
+			result_ = multop::instance(mo->op(), res);
+			spot::ltl::destroy(mo);
+			return;
+		      }
+		    if (is_GF(mo->nth(1)))
+		      {
+			multop::vec* res = new multop::vec;
+			res->push_back(unop::instance(unop::F,
+						      basic_reduce_form(mo->nth(0))));
+			res->push_back(basic_reduce_form(mo->nth(1)));
+			result_ = multop::instance(mo->op(), res);
+			spot::ltl::destroy(mo);
+			return;
+		      }
 		  }
-		  if (is_GF(dynamic_cast<multop*>(result_)->nth(1))) {
-		    //|| is_FG(dynamic_cast<multop*>(result_)->nth(1))) {
-		    multop::vec* res = new multop::vec;
-		    res->push_back(unop::instance(unop::G, basic_reduce_form(dynamic_cast<multop*>(result_)->nth(0))));
-		    res->push_back(basic_reduce_form(dynamic_cast<multop*>(result_)->nth(1)));
-		    spot::ltl::destroy(result_);
-		    result_ = multop::instance(multop::Or, res);
-		    return;
-		  }
-		}
 	      }
-	    }
+
 
 	    result_ = unop::instance(unop::G, result_);
 	    return;
@@ -230,6 +245,8 @@ namespace spot
 	formula* ftmp = NULL;
 	node_type_form_visitor v1;
 	node_type_form_visitor v2;
+	unop* fu1 = NULL;
+	unop* fu2 = NULL;
 	switch (bo->op())
 	  {
 	  case binop::Xor:
@@ -252,28 +269,31 @@ namespace spot
 
 	    /* a U false = false
 	       a U true = true */
-	    if (node_type(f2) == (node_type_form_visitor::Const)) {
-	      result_ = f2;
-	      return;
-	    }
+	    if (node_type(f2) == (node_type_form_visitor::Const))
+	      {
+		result_ = f2;
+		return;
+	      }
 
 	    f1 = basic_reduce_form(f1);
 
 	    /* X(a) U X(b) = X(a U b) */
-	    if ( node_type(f1) == (node_type_form_visitor::Unop)
-		 && node_type(f2) == (node_type_form_visitor::Unop)) {
-	      if ((dynamic_cast<unop*>(f1)->op() == unop::X)
-		  && (dynamic_cast<unop*>(f2)->op() == unop::X)) {
+	    fu1 = dynamic_cast<unop*>(f1);
+	    fu2 = dynamic_cast<unop*>(f2);
+	    if ((fu1 && fu2) &&
+		(fu1->op() == unop::X) &&
+		(fu2->op() == unop::X))
+	      {
 		ftmp = binop::instance(binop::U,
-				       basic_reduce_form(dynamic_cast<unop*>(f1)->child()),
-				       basic_reduce_form(dynamic_cast<unop*>(f2)->child()));
+				       basic_reduce_form(fu1->child()),
+				       basic_reduce_form(fu2->child()));
 		result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
 		spot::ltl::destroy(f1);
 		spot::ltl::destroy(f2);
 		spot::ltl::destroy(ftmp);
 		return;
 	      }
-	    }
+
 	    result_ = binop::instance(binop::U, f1, f2);
 	    return;
 
@@ -282,28 +302,31 @@ namespace spot
 
 	    /* a R false = false
 	       a R true = true */
-	    if (node_type(f2) == (node_type_form_visitor::Const)) {
-	      result_ = f2;
-	      return;
-	    }
+	    if (node_type(f2) == (node_type_form_visitor::Const))
+	      {
+		result_ = f2;
+		return;
+	      }
 
 	    f1 = basic_reduce_form(f1);
 
 	    /* X(a) R X(b) = X(a R b) */
-	    if (node_type(f1) == (node_type_form_visitor::Unop)
-		&& node_type(f2) == (node_type_form_visitor::Unop)) {
-	      if ((dynamic_cast<unop*>(f1)->op() == unop::X)
-		  && (dynamic_cast<unop*>(f2)->op() == unop::X)) {
+	    fu1 = dynamic_cast<unop*>(f1);
+	    fu2 = dynamic_cast<unop*>(f2);
+	    if ((fu1 && fu2) &&
+		(fu1->op() == unop::X) &&
+		(fu2->op() == unop::X))
+	      {
 		ftmp = binop::instance(bo->op(),
-				       basic_reduce_form(dynamic_cast<unop*>(f1)->child()),
-				       basic_reduce_form(dynamic_cast<unop*>(f2)->child()));
+				       basic_reduce_form(fu1->child()),
+				       basic_reduce_form(fu2->child()));
 		result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
 		spot::ltl::destroy(f1);
 		spot::ltl::destroy(f2);
 		spot::ltl::destroy(ftmp);
 		return;
-	      }
 	    }
+
 	    result_ = binop::instance(bo->op(),
 				      f1, f2);
 	    return;
@@ -330,6 +353,9 @@ namespace spot
 
 	multop::vec* tmpOther = new multop::vec;
 
+	unop* uo = NULL;
+	unop* uo2 = NULL;
+	binop* bo = NULL;
 	formula* ftmp = NULL;
 
 	for (unsigned i = 0; i < mos; ++i)
@@ -340,96 +366,107 @@ namespace spot
 	  {
 	  case multop::And:
 
-	    for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
-	      if (*i == NULL) continue;
-	      switch (node_type(*i)) {
+	    for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
+	      {
+		if (*i == NULL)
+		  continue;
+		switch (node_type(*i))
+		  {
 
-	      case node_type_form_visitor::Unop:
+		  case node_type_form_visitor::Unop:
 
-		/* Xa & Xb = X(a & b)*/
-		if (dynamic_cast<unop*>(*i)->op() == unop::X) {
-		  tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(*i)->child()));
-		  break;
-		}
+		    /* Xa & Xb = X(a & b)*/
+		    uo = dynamic_cast<unop*>(*i);
+		    if (uo && uo->op() == unop::X)
+		      {
+			tmpX->push_back(basic_reduce_form(uo->child()));
+			break;
+		      }
 
-		/* FG(a) & FG(b) = FG(a & b)*/
-		if (is_FG(*i)) {
-		  tmpFG->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(dynamic_cast<unop*>(*i)->child())->child()));
-		  break;
-		}
-		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
-		break;
-		/* A GERER !!!!!!!!!!!!!!!!!!!!!!!
-		   case node_type_form_visitor::Const:
-		   tmpX->push_back( spot::ltl::clone((*i)) );
-		   break;
-		*/
+		    /* FG(a) & FG(b) = FG(a & b)*/
+		    if (is_FG(*i))
+		      {
+			uo2 = dynamic_cast<unop*>(uo->child());
+			tmpFG->push_back(basic_reduce_form(uo2->child()));
+			break;
+		      }
+		    tmpOther->push_back(basic_reduce_form(*i));
+		    break;
 
-	      case node_type_form_visitor::Binop:
+		  case node_type_form_visitor::Binop:
 
-		/* (a U b) & (c U b) = (a & c) U b */
-		if (dynamic_cast<binop*>(*i)->op() == binop::U) {
-		  ftmp = dynamic_cast<binop*>(*i)->second();
-		  tmpUright = new multop::vec;
-		  for (multop::vec::iterator j = i; j != res->end(); j++)
-		    {
-		      if (*j == NULL) continue;
-		      if (node_type(*j) == node_type_form_visitor::Binop)
-			{
-			  if (dynamic_cast<binop*>(*j)->op() == binop::U)
-			    {
-			      if (ftmp == dynamic_cast<binop*>(*j)->second())
-				{
-				  tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->first() ));
-				  if (j != i) {
+		    /* (a U b) & (c U b) = (a & c) U b */
+		    if (dynamic_cast<binop*>(*i)->op() == binop::U)
+		      {
+			ftmp = dynamic_cast<binop*>(*i)->second();
+			tmpUright = new multop::vec;
+			for (multop::vec::iterator j = i; j != res->end(); j++)
+			  {
+			    if (*j == NULL) continue;
+			    if ((node_type(*j) == node_type_form_visitor::Binop)
+				&&
+				(dynamic_cast<binop*>(*j)->op() == binop::U) &&
+				(ftmp == dynamic_cast<binop*>(*j)->second()))
+			      {
+				bo = dynamic_cast<binop*>(*j);
+				tmpUright
+				  ->push_back(basic_reduce_form(bo->first()));
+				if (j != i)
+				  {
+				    destroy(*j);
+				    *j = NULL;
+				  }
+			      }
+			  }
+			tmpU
+			  ->push_back(binop::instance(binop::U,
+						      multop::
+						      instance(multop::
+							       And,
+							       tmpUright),
+						      basic_reduce_form(ftmp)));
+			break;
+		      }
+
+		    /* (a R b) & (a R c) = a R (b & c) */
+		    if (dynamic_cast<binop*>(*i)->op() == binop::R)
+		      {
+			ftmp = dynamic_cast<binop*>(*i)->first();
+			tmpRright = new multop::vec;
+			for (multop::vec::iterator j = i; j != res->end(); j++)
+			  {
+			    if (*j == NULL) continue;
+			    if ((node_type(*j) == node_type_form_visitor::Binop)
+				&&
+				(dynamic_cast<binop*>(*j)->op() == binop::R) &&
+				(ftmp == dynamic_cast<binop*>(*j)->first()))
+			      {
+				bo = dynamic_cast<binop*>(*j);
+				tmpRright
+				  ->push_back(basic_reduce_form(bo->second()));
+				if (j != i)
+				  {
 				    spot::ltl::destroy(*j);
 				    *j = NULL;
 				  }
-				}
-			    }
-			}
-		    }
-		  tmpU->push_back(binop::instance(binop::U,
-						  multop::instance(multop::And,tmpUright),
-						  basic_reduce_form(ftmp)));
-		  break;
-		}
-
-		/* (a R b) & (a R c) = a R (b & c) */
-		if (dynamic_cast<binop*>(*i)->op() == binop::R) {
-		  ftmp = dynamic_cast<binop*>(*i)->first();
-		  tmpRright = new multop::vec;
-		  for (multop::vec::iterator j = i; j != res->end(); j++)
-		    {
-		      if (*j == NULL) continue;
-		      if (node_type(*j) == node_type_form_visitor::Binop)
-			{
-			  if (dynamic_cast<binop*>(*j)->op() == binop::R)
-			    {
-			      if (ftmp == dynamic_cast<binop*>(*j)->first())
-				{
-				  tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->second() ));
-				  if (j != i) {
-				    spot::ltl::destroy(*j);
-				    *j = NULL;
-				  }
-				}
-			    }
-			}
-		    }
-		  tmpR->push_back(binop::instance(binop::R,
-						  basic_reduce_form(ftmp),
-						  multop::instance(multop::And,tmpRright)));
-		  break;
-		}
-		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
-		break;
-	      default:
-		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
-		break;
+			      }
+			  }
+			tmpR
+			  ->push_back(binop::instance(binop::R,
+						      basic_reduce_form(ftmp),
+						      multop::
+						      instance(multop::And,
+							       tmpRright)));
+			break;
+		      }
+		    tmpOther->push_back(basic_reduce_form(*i));
+		    break;
+		  default:
+		    tmpOther->push_back(basic_reduce_form(*i));
+		    break;
+		  }
+		spot::ltl::destroy(*i);
 	      }
-	      spot::ltl::destroy(*i);
-	    }
 
 	    delete(tmpGF);
 	    tmpGF = NULL;
@@ -438,91 +475,104 @@ namespace spot
 
 	  case multop::Or:
 
-	    for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
-	      if (*i == NULL) continue;
-	      switch (node_type(*i)) {
+	    for (multop::vec::iterator i = res->begin(); i != res->end(); i++)
+	      {
+		if (*i == NULL) continue;
+		switch (node_type(*i))
+		  {
 
-	      case node_type_form_visitor::Unop:
+		  case node_type_form_visitor::Unop:
 
-		/* Xa | Xb = X(a | b)*/
-		if (dynamic_cast<unop*>(*i)->op() == unop::X) {
-		  tmpX->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(*i)->child()));
-		  break;
-		}
+		    /* Xa | Xb = X(a | b)*/
+		    uo = dynamic_cast<unop*>(*i);
+		    if (uo && uo->op() == unop::X)
+		      {
+			tmpX->push_back(basic_reduce_form(uo->child()));
+			break;
+		      }
 
-		/* GF(a) | GF(b) = GF(a | b)*/
-		if (is_GF(*i)) {
-		  tmpGF->push_back(spot::ltl::basic_reduce_form(dynamic_cast<unop*>(dynamic_cast<unop*>(*i)->child())->child()));
-		  break;
-		}
-		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
-		break;
+		    /* GF(a) | GF(b) = GF(a | b)*/
+		    if (is_GF(*i))
+		      {
+			uo2 = dynamic_cast<unop*>(uo->child());
+			tmpGF->push_back(basic_reduce_form(uo2->child()));
+			break;
+		      }
+		    tmpOther->push_back(basic_reduce_form(*i));
+		    break;
 
-	      case node_type_form_visitor::Binop:
+		  case node_type_form_visitor::Binop:
 
-		/* (a U b) | (a U c) = a U (b | c) */
-		if (dynamic_cast<binop*>(*i)->op() == binop::U) {
-		  ftmp = dynamic_cast<binop*>(*i)->first();
-		  tmpUright = new multop::vec;
-		  for (multop::vec::iterator j = i; j != res->end(); j++)
-		    {
-		      if (*j == NULL) continue;
-		      if (node_type(*j) == node_type_form_visitor::Binop)
-			{
-			  if (dynamic_cast<binop*>(*j)->op() == binop::U)
-			    {
-			      if (ftmp == dynamic_cast<binop*>(*j)->first())
-				{
-				  tmpUright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->second()));
-				  if (j != i) {
-				    spot::ltl::destroy(*j);
+		    /* (a U b) | (a U c) = a U (b | c) */
+		    if (dynamic_cast<binop*>(*i)->op() == binop::U)
+		      {
+			ftmp = dynamic_cast<binop*>(*i)->first();
+			tmpUright = new multop::vec;
+			for (multop::vec::iterator j = i; j != res->end(); j++)
+			  {
+			    if (*j == NULL) continue;
+			    if ((node_type(*j) == node_type_form_visitor::Binop)
+				&&
+				(dynamic_cast<binop*>(*j)->op() == binop::U) &&
+				(ftmp == dynamic_cast<binop*>(*j)->first()))
+			      {
+				bo = dynamic_cast<binop*>(*j);
+				tmpUright
+				  ->push_back(basic_reduce_form(bo->second()));
+				if (j != i)
+				  {
+				    destroy(*j);
 				    *j = NULL;
 				  }
-				}
-			    }
-			}
-		    }
-		  tmpU->push_back(binop::instance(binop::U,
-						  basic_reduce_form(ftmp),
-						  multop::instance(multop::Or,tmpUright)));
-		  break;
-		}
+			      }
+			  }
+			tmpU->push_back(binop::instance(binop::U,
+							basic_reduce_form(ftmp),
+							multop::
+							instance(multop::Or,
+								 tmpUright)));
+			break;
+		      }
 
-		/* (a R b) | (c R b) = (a | c) R b */
-		if (dynamic_cast<binop*>(*i)->op() == binop::R) {
-		  ftmp = dynamic_cast<binop*>(*i)->second();
-		  tmpRright = new multop::vec;
-		  for (multop::vec::iterator j = i; j != res->end(); j++)
-		    {
-		      if (*j == NULL) continue;
-		      if (node_type(*j) == node_type_form_visitor::Binop)
-			{
-			  if (dynamic_cast<binop*>(*j)->op() == binop::R)
-			    {
-			      if (ftmp == dynamic_cast<binop*>(*j)->second())
-				{
-				  tmpRright->push_back(spot::ltl::basic_reduce_form(dynamic_cast<binop*>(*j)->first()));
-				  if (j != i) {
-				    spot::ltl::destroy(*j);
+		    /* (a R b) | (c R b) = (a | c) R b */
+		    if (dynamic_cast<binop*>(*i)->op() == binop::R)
+		      {
+			ftmp = dynamic_cast<binop*>(*i)->second();
+			tmpRright = new multop::vec;
+			for (multop::vec::iterator j = i; j != res->end(); j++)
+			  {
+			    if (*j == NULL) continue;
+			    if ((node_type(*j) == node_type_form_visitor::Binop)
+				&&
+				(dynamic_cast<binop*>(*j)->op() == binop::R) &&
+				(ftmp == dynamic_cast<binop*>(*j)->second()))
+			      {
+				bo = dynamic_cast<binop*>(*j);
+				tmpRright
+				  ->push_back(basic_reduce_form(bo->first()));
+				if (j != i)
+				  {
+				    destroy(*j);
 				    *j = NULL;
 				  }
-				}
-			    }
-			}
-		    }
-		  tmpR->push_back(binop::instance(binop::R,
-						  multop::instance(multop::Or,tmpRright),
-						  basic_reduce_form(ftmp)));
-		  break;
-		}
-		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
-		break;
-	      default:
-		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
-		break;
+			      }
+			  }
+			tmpR
+			  ->push_back(binop::instance(binop::R,
+						      multop::
+						      instance(multop::Or,
+							       tmpRright),
+						      basic_reduce_form(ftmp)));
+			break;
+		      }
+		    tmpOther->push_back(basic_reduce_form(*i));
+		    break;
+		  default:
+		    tmpOther->push_back(basic_reduce_form(*i));
+		    break;
+		  }
+		spot::ltl::destroy(*i);
 	      }
-	      spot::ltl::destroy(*i);
-	    }
 
 	    delete(tmpFG);
 	    tmpFG = NULL;
@@ -535,27 +585,37 @@ namespace spot
 	delete(res);
 
 	if (tmpX->size())
-	  tmpOther->push_back(unop::instance(unop::X,multop::instance(mo->op(),tmpX)));
+	  tmpOther->push_back(unop::instance(unop::X,
+					     multop::instance(mo->op(),
+							      tmpX)));
 	else delete(tmpX);
 
 	if (tmpU->size())
-	  tmpOther->push_back(multop::instance(mo->op(),tmpU));
+	  tmpOther->push_back(multop::instance(mo->op(), tmpU));
 	else delete(tmpU);
 
 	if (tmpR->size())
-	  tmpOther->push_back(multop::instance(mo->op(),tmpR));
+	  tmpOther->push_back(multop::instance(mo->op(), tmpR));
 	else delete(tmpR);
 
-	if (tmpGF != NULL)
-	  if (tmpGF->size())
-	    tmpOther->push_back(unop::instance(unop::G,
-					       unop::instance(unop::F,
-							      multop::instance(mo->op(),tmpGF))));
-	if (tmpFG != NULL)
-	  if (tmpFG->size())
-	    tmpOther->push_back(unop::instance(unop::F,
-					       unop::instance(unop::G,
-							      multop::instance(mo->op(),tmpFG))));
+	if ((tmpGF != NULL) &&
+	    (tmpGF->size()))
+	  {
+	    ftmp = unop::instance(unop::G,
+				  unop::instance(unop::F,
+						 multop::instance(mo->op(),
+								  tmpGF)));
+	    tmpOther->push_back(ftmp);
+	  }
+	if ((tmpFG != NULL) &&
+	    (tmpFG->size()))
+	  {
+	    ftmp = unop::instance(unop::F,
+				  unop::instance(unop::G,
+						 multop::instance(mo->op(),
+								  tmpFG)));
+	    tmpOther->push_back(ftmp);
+	  }
 
 	result_ = multop::instance(op, tmpOther);
 
diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc
index aefd51fb1..282c123f4 100644
--- a/src/ltlvisit/reducform.cc
+++ b/src/ltlvisit/reducform.cc
@@ -91,13 +91,13 @@ namespace spot
 
 	  case unop::F:
 	    /* If f is class of eventuality then F(f)=f.  */
-	    if (!is_eventual(result_) || (o == Inf))
+	    if (!is_eventual(result_) || o == Inf || o == InfBase)
 	      result_ = unop::instance(unop::F, result_);
 	    return;
 
 	  case unop::G:
 	    /* If f is class of universality then G(f)=f.  */
-	    if (!is_universal(result_) || (o == Inf))
+	    if (!is_universal(result_) || o == Inf || o == InfBase)
 	      result_ = unop::instance(unop::G, result_);
 	    return;
 	  }
@@ -112,7 +112,7 @@ namespace spot
 
 	/* If b is of class eventuality then a U b = b.
 	   If b is of class universality then a R b = b. */
-	if ((o != Inf)
+	if ((o != Inf) && (o != InfBase)
 	    && ((is_eventual(f2) && ((bo->op()) == binop::U))
 		|| (is_universal(f2) && ((bo->op()) == binop::R))))
 	  {
@@ -122,7 +122,7 @@ namespace spot
 	/* case of implies */
 	formula* f1 = recurse(bo->first());
 
-	if (o != EventualUniversal)
+	if (o != EventualUniversal && o != EventualUniversalBase)
 	  {
 	    bool inf = inf_form(f1, f2);
 	    bool infinv = inf_form(f2, f1);
@@ -206,7 +206,7 @@ namespace spot
 	for (unsigned i = 0; i < mos; ++i)
 	  res->push_back(recurse(mo->nth(i)));
 
-	if (o != EventualUniversal)
+	if (o != EventualUniversal && o != EventualUniversalBase)
 	  {
 	    switch (mo->op())
 	      {
@@ -312,7 +312,8 @@ namespace spot
       spot::ltl::formula* ftmp2 = NULL;
       reduce_form_visitor v(o);
 
-      if (o == BRI)
+      if (o == BRI || o == InfBase ||
+	  o == EventualUniversalBase)
 	{
 	  ftmp1 = spot::ltl::basic_reduce_form(f);
 	  const_cast<formula*>(ftmp1)->accept(v);
@@ -350,11 +351,20 @@ namespace spot
 	case Inf:
 	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
 	  break;
+	case InfBase:
+	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
+	  break;
 	case EventualUniversal:
 	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
 	  break;
+	case EventualUniversalBase:
+	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
+	  break;
+	case InfEventualUniversal:
+	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
+	  break;
 	case BRI:
-	  ftmp3 = spot::ltl::reduce_form(ftmp2);
+	  ftmp3 = spot::ltl::reduce_form(ftmp2, o);
 	  break;
 	default:
 	  assert(0);
diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh
index 8a34547f9..bdc087a46 100644
--- a/src/ltlvisit/reducform.hh
+++ b/src/ltlvisit/reducform.hh
@@ -42,7 +42,13 @@ namespace spot
     /// EventualUniversal for spot::ltl::reduce_eventuality_universality_form,
     /// BRI for spot::ltl::reduce_form.
 
-    enum option {Base, Inf, EventualUniversal, BRI};
+    enum option {Base,
+		 Inf,
+		 InfBase,
+		 EventualUniversal,
+		 EventualUniversalBase,
+		 InfEventualUniversal,
+		 BRI};
     formula* reduce(const formula* f, option o = BRI);
 
     /// Implement basic rewriting.
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 735968a2e..6dcc47e2b 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -352,12 +352,19 @@ main(int argc, char** argv)
 	  else if (reduc_r1 | reduc_r2 | reduc_r3)
 	    {
 	      spot::ltl::option o = spot::ltl::BRI;
-	      if (reduc_r1)
+	      if (reduc_r1 & !reduc_r2 & !reduc_r3)
 		o = spot::ltl::Base;
-	      if (reduc_r2)
+	      if (!reduc_r1 & reduc_r2 & !reduc_r3)
 		o = spot::ltl::EventualUniversal;
-	      if (reduc_r3)
+	      if (reduc_r1 & reduc_r2 & !reduc_r3)
+		o = spot::ltl::EventualUniversalBase;
+	      if (!reduc_r1 & !reduc_r2 & reduc_r3)
 		o = spot::ltl::Inf;
+	      if (reduc_r1 & !reduc_r2 & reduc_r3)
+		o = spot::ltl::InfBase;
+	      if (!reduc_r1 & reduc_r2 & reduc_r3)
+		o = spot::ltl::InfEventualUniversal;
+
 	      f = spot::ltl::reduce(f, o);
 	    }