diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 0d7df47dd..b5c91c85f 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -121,6 +121,16 @@ namespace spot
 	opt.containment_checks |= opt.containment_checks_stronger;
       }
 
+      void
+      print_stats(std::ostream& os) const
+      {
+	os << "simplified formulae:    " << simplified_.size() << " entries\n"
+	   << "negative normal form:   " << nenoform_.size() << " entries\n"
+	   << "syntactic implications: " << syntimpl_.size() << " entries\n"
+	   << "boolean to bdd:         " << as_bdd_.size() << " entries\n"
+	   << "star normal form:       " << snf_cache_.size() << " entries\n";
+      }
+
       // Convert a Boolean formula into a BDD for easier comparison.
       bdd
       as_bdd(const formula* f)
@@ -4249,5 +4259,12 @@ namespace spot
       return cache_->dict;
     }
 
+    void
+    ltl_simplifier::print_stats(std::ostream& os) const
+    {
+      cache_->print_stats(os);
+    }
+
+
   }
 }
diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh
index 1b4775eaa..142c88c7f 100644
--- a/src/ltlvisit/simplify.hh
+++ b/src/ltlvisit/simplify.hh
@@ -24,6 +24,7 @@
 #include "ltlast/formula.hh"
 #include "bdd.h"
 #include "tgba/bdddict.hh"
+#include <iosfwd>
 
 namespace spot
 {
@@ -136,6 +137,9 @@ namespace spot
       /// Cached version of spot::ltl::star_normal_form().
       const formula* star_normal_form(const formula* f);
 
+      /// Dump statistics about the caches.
+      void print_stats(std::ostream& os) const;
+
     private:
       ltl_simplifier_cache* cache_;
       // Copy disallowed.
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index a787367ef..cd59dd569 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -177,6 +177,7 @@ syntax(char* prog)
 	    << "  -r6   reduce formula using tau03+" << std::endl
 	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
 	    << "  -rd   display the reduced formula" << std::endl
+	    << "  -rD   dump statistics about the simplifier cache" << std::endl
 	    << "  -rL   disable basic rewritings producing larger formulas"
 	    << std::endl << std::endl
 
@@ -305,6 +306,7 @@ main(int argc, char** argv)
   bool simpltl = false;
   spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
 					   false, false, false);
+  bool simpcache_stats = false;
   bool scc_filter_all = false;
   bool symbolic_scc_pruning = false;
   bool display_reduced_form = false;
@@ -619,6 +621,10 @@ main(int argc, char** argv)
 	{
 	  display_reduced_form = true;
 	}
+      else if (!strcmp(argv[formula_index], "-rD"))
+	{
+	  simpcache_stats = true;
+	}
       else if (!strcmp(argv[formula_index], "-RDS"))
         {
           reduction_dir_sim = true;
@@ -879,6 +885,23 @@ main(int argc, char** argv)
 	  tm.stop("translating formula");
 	  to_free = a;
 
+	  if (simp && simpcache_stats)
+	    {
+	      simp->print_stats(std::cerr);
+	      bddStat s;
+	      bdd_stats(&s);
+	      std::cerr << "BDD produced: " << s.produced
+			<< "\n    nodenum: " << s.nodenum
+			<< "\n    maxnodenum: " << s.maxnodenum
+			<< "\n    freenodes: " <<  s.freenodes
+			<< "\n    minfreenodes: " << s.minfreenodes
+			<< "\n    varnum: " <<  s.varnum
+			<< "\n    cachesize: " << s.cachesize
+			<< "\n    gbcnum: " << s.gbcnum
+			<< std::endl;
+	      bdd_fprintstat(stderr);
+	      dict->dump(std::cerr);
+	    }
 	  delete simp;
 	}