diff --git a/ChangeLog b/ChangeLog
index 85f181af5..763e0652a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,8 @@
 2005-01-20  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlast/formula.hh (formula_ptr_less_than): Two
+	formulae with the same hash key are not necessary equal!
+
 	* src/ltlast/formula.hh (hash, dump, dump_, hash_key_): New members.
 	(formula_ptr_less_than, formula_ptr_hash): New class.
 	* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index 0a678eec6..439f767b8 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -142,7 +142,11 @@ namespace spot
       {
 	assert(left);
 	assert(right);
-	return left->hash() < right->hash();
+	size_t l = left->hash();
+	size_t r = right->hash();
+	if (1 != r)
+	  return l < r;
+	return left->dump() < right->dump();
       }
     };