diff --git a/ChangeLog b/ChangeLog
index 632b0eb81..32324b245 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,11 +1,11 @@
 2003-06-30  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
-	* src/tgba/tgbabddconcretefactory.cc: 
+	* src/tgba/tgbabddconcretefactory.cc:
 	(tgba_bdd_concrete_factory::tgba_bdd_concrete_factory): New.
 	(tgba_bdd_concrete_factory::create_state): Update now_to_next_.
 	(tgba_bdd_concrete_factory::finish): Constraint Next variables
 	in the relation.
-	* src/tgba/tgbabddconcretefactory.hh 
+	* src/tgba/tgbabddconcretefactory.hh
 	(tgba_bdd_concrete_factory::now_to_next_): New variable.
 
 2003-06-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc
index b5f447d9d..f2600297b 100644
--- a/src/tgba/tgbabddconcretefactory.cc
+++ b/src/tgba/tgbabddconcretefactory.cc
@@ -3,6 +3,11 @@
 #include "tgbabddconcretefactory.hh"
 namespace spot
 {
+  tgba_bdd_concrete_factory::tgba_bdd_concrete_factory()
+    : now_to_next_(bdd_newpair())
+  {
+  }
+
   tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory()
   {
     acc_map_::iterator ai;
@@ -27,6 +32,7 @@ namespace spot
     // Record that num+1 should be renamed as num when
     // the next state becomes current.
     bdd_setpair(data_.next_to_now, num + 1, num);
+    bdd_setpair(now_to_next_, num, num + 1);
 
     // Keep track of all "Now" variables for easy
     // existential quantification.
@@ -100,6 +106,15 @@ namespace spot
 	// of this accepting set.
 	data_.accepting_conditions |= ai->second & acc;
       }
+
+    // Any constraint between Now variables also exist between Next
+    // variables.  Doing this limits the quantity of useless
+    // successors we will have to explore.  (By "useless successors"
+    // I mean a combination of Next variables that represent a cul de sac
+    // state: the combination exists but won't allow further exploration
+    // because it fails the constraints.)
+    data_.relation &= bdd_replace(bdd_exist(data_.relation, data_.notnow_set),
+				  now_to_next_);
   }
 
   const tgba_bdd_core_data&
diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh
index 83ac08e39..c73f1d1f5 100644
--- a/src/tgba/tgbabddconcretefactory.hh
+++ b/src/tgba/tgbabddconcretefactory.hh
@@ -69,7 +69,7 @@ namespace spot
     typedef std::map<const ltl::formula*, bdd> acc_map_;
     acc_map_ acc_;		///< BDD associated to each accepting condition
     bddPair *now_to_next_;	///< \brief Rewriting pairs to transform
-                                ///  Now variables into Next variables.
+				///  Now variables into Next variables.
   };
 
 }