diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc
index 6237236f9..16b4b8ca8 100644
--- a/iface/dve2/dve2.cc
+++ b/iface/dve2/dve2.cc
@@ -328,7 +328,7 @@ namespace spot
     int
     convert_aps(const ltl::atomic_prop_set* aps,
 		const dve2_interface* d,
-		bdd_dict* dict,
+		bdd_dict_ptr dict,
 		const ltl::formula* dead,
 		prop_set& out)
     {
@@ -604,8 +604,8 @@ namespace spot
     {
     public:
 
-      dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps,
-		  const ltl::formula* dead, int compress)
+      dve2_kripke(const dve2_interface* d, bdd_dict_ptr dict,
+		  const prop_set* ps, const ltl::formula* dead, int compress)
 	: d_(d),
 	  state_size_(d_->get_state_variable_count()),
 	  dict_(dict), ps_(ps),
@@ -913,7 +913,7 @@ namespace spot
       }
 
       virtual
-      spot::bdd_dict* get_dict() const
+      spot::bdd_dict_ptr get_dict() const
       {
 	return dict_;
       }
@@ -921,7 +921,7 @@ namespace spot
     private:
       const dve2_interface* d_;
       int state_size_;
-      bdd_dict* dict_;
+      bdd_dict_ptr dict_;
       const char** vname_;
       bool* format_filter_;
       const prop_set* ps_;
@@ -998,7 +998,7 @@ namespace spot
 
 
   kripke*
-  load_dve2(const std::string& file_arg, bdd_dict* dict,
+  load_dve2(const std::string& file_arg, bdd_dict_ptr dict,
 	    const ltl::atomic_prop_set* to_observe,
 	    const ltl::formula* dead,
 	    int compress,
diff --git a/iface/dve2/dve2.hh b/iface/dve2/dve2.hh
index 0fec5807b..3ff562118 100644
--- a/iface/dve2/dve2.hh
+++ b/iface/dve2/dve2.hh
@@ -1,5 +1,6 @@
-// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement
-// de l'Epita (LRDE)
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -56,7 +57,7 @@ namespace spot
   //         dead states
   // \a verbose whether to output verbose messages
   SPOT_API kripke*
-  load_dve2(const std::string& file, bdd_dict* dict,
+  load_dve2(const std::string& file, bdd_dict_ptr dict,
 	    const ltl::atomic_prop_set* to_observe,
 	    const ltl::formula* dead = ltl::constant::true_instance(),
 	    int compress = 0, bool verbose = true);
diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc
index a1c95bac5..f3913b4a3 100644
--- a/iface/dve2/dve2check.cc
+++ b/iface/dve2/dve2check.cc
@@ -156,7 +156,7 @@ main(int argc, char **argv)
 
 
   spot::ltl::atomic_prop_set ap;
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
   spot::kripke* model = 0;
   const spot::tgba* prop = 0;
   spot::tgba* product = 0;
@@ -367,7 +367,6 @@ main(int argc, char **argv)
   delete model;
   if (f)
     f->destroy();
-  delete dict;
 
   deadf->destroy();
 
diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc
index 5992d442d..b3a0c35bc 100644
--- a/src/bin/dstar2tgba.cc
+++ b/src/bin/dstar2tgba.cc
@@ -293,8 +293,7 @@ namespace
     {
       spot::dstar_parse_error_list pel;
       spot::dstar_aut* daut;
-      spot::bdd_dict dict;
-      daut = spot::dstar_parse(filename, pel, &dict);
+      daut = spot::dstar_parse(filename, pel, spot::make_bdd_dict());
       if (spot::format_dstar_parse_errors(std::cerr, filename, pel))
 	{
 	  delete daut;
diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 33208dee7..8005b3878 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -739,7 +739,7 @@ namespace
   class translator_runner: protected spot::formater
   {
   private:
-    spot::bdd_dict& dict;
+    spot::bdd_dict_ptr dict;
     // Round-specific variables
     quoted_string string_ltl_spot;
     quoted_string string_ltl_spin;
@@ -754,7 +754,7 @@ namespace
   public:
     using spot::formater::has;
 
-    translator_runner(spot::bdd_dict& dict)
+    translator_runner(spot::bdd_dict_ptr dict)
       : dict(dict)
     {
       declare('f', &string_ltl_spot);
@@ -902,7 +902,7 @@ namespace
 	      {
 		spot::neverclaim_parse_error_list pel;
 		std::string filename = output.val()->name();
-		res = spot::neverclaim_parse(filename, pel, &dict);
+		res = spot::neverclaim_parse(filename, pel, dict);
 		if (!pel.empty())
 		  {
 		    status_str = "parse error";
@@ -930,7 +930,7 @@ namespace
 		  }
 		else
 		  {
-		    res = spot::lbtt_parse(f, error, &dict);
+		    res = spot::lbtt_parse(f, error, dict);
 		    if (!res)
 		      {
 			status_str = "parse error";
@@ -948,7 +948,7 @@ namespace
 		spot::dstar_parse_error_list pel;
 		std::string filename = output.val()->name();
 		spot::dstar_aut* aut;
-		aut = spot::dstar_parse(filename, pel, &dict);
+		aut = spot::dstar_parse(filename, pel, dict);
 		if (!pel.empty())
 		  {
 		    status_str = "parse error";
@@ -1191,12 +1191,12 @@ namespace
 
   class processor: public job_processor
   {
-    spot::bdd_dict dict;
+    spot::bdd_dict_ptr dict = spot::make_bdd_dict();
     translator_runner runner;
     fset_t unique_set;
   public:
-    processor()
-      : runner(dict)
+    processor():
+      runner(dict)
     {
     }
 
@@ -1401,7 +1401,7 @@ namespace
 	  // build a random state-space.
 	  spot::srand(seed);
 	  spot::tgba* statespace = spot::random_graph(states, density,
-						      ap, &dict);
+						      ap, dict);
 
 	  // Products of the state space with the positive automata.
 	  std::vector<spot::tgba*> pos_prod(m);
diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy
index dded9fdf9..3b6c02f7b 100644
--- a/src/dstarparse/dstarparse.yy
+++ b/src/dstarparse/dstarparse.yy
@@ -279,7 +279,7 @@ states:
 
 static void fill_guards(result_& r)
 {
-  spot::bdd_dict* d = r.d->aut->get_dict();
+  spot::bdd_dict_ptr d = r.d->aut->get_dict();
 
   size_t nap = r.aps.size();
   int* vars = new int[nap];
@@ -316,7 +316,7 @@ namespace spot
   dstar_aut*
   dstar_parse(const std::string& name,
 	      dstar_parse_error_list& error_list,
-	      bdd_dict* dict,
+	      bdd_dict_ptr dict,
 	      ltl::environment& env,
 	      bool debug)
   {
diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh
index ce03eecc2..440db7e1f 100644
--- a/src/dstarparse/public.hh
+++ b/src/dstarparse/public.hh
@@ -88,7 +88,7 @@ namespace spot
   SPOT_API dstar_aut*
   dstar_parse(const std::string& filename,
 	      dstar_parse_error_list& error_list,
-	      bdd_dict* dict,
+	      bdd_dict_ptr dict,
 	      ltl::environment& env = ltl::default_environment::instance(),
 	      bool debug = false);
 
diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/tgbagraph.cc
index 694b50ab9..f4fa3ce16 100644
--- a/src/graphtest/tgbagraph.cc
+++ b/src/graphtest/tgbagraph.cc
@@ -25,18 +25,18 @@
 
 void f1()
 {
-  spot::bdd_dict d;
+  auto d = spot::make_bdd_dict();
 
   auto& e = spot::ltl::default_environment::instance();
 
-  spot::tgba_digraph tg(&d);
+  spot::tgba_digraph tg(d);
 
   auto* f1 = e.require("p1");
   auto* f2 = e.require("p2");
-  bdd p1 = bdd_ithvar(d.register_proposition(f1, &tg));
-  bdd p2 = bdd_ithvar(d.register_proposition(f2, &tg));
-  bdd a1 = bdd_ithvar(d.register_acceptance_variable(f1, &tg));
-  bdd a2 = bdd_ithvar(d.register_acceptance_variable(f2, &tg));
+  bdd p1 = bdd_ithvar(d->register_proposition(f1, &tg));
+  bdd p2 = bdd_ithvar(d->register_proposition(f2, &tg));
+  bdd a1 = bdd_ithvar(d->register_acceptance_variable(f1, &tg));
+  bdd a2 = bdd_ithvar(d->register_acceptance_variable(f2, &tg));
   f1->destroy();
   f2->destroy();
 
diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc
index c0cbe9b7b..16223912a 100644
--- a/src/kripke/kripkeexplicit.cc
+++ b/src/kripke/kripkeexplicit.cc
@@ -126,13 +126,13 @@ namespace spot
   // kripke_explicit
 
 
-  kripke_explicit::kripke_explicit(bdd_dict* dict)
+  kripke_explicit::kripke_explicit(bdd_dict_ptr dict)
     : dict_(dict),
       init_(0)
   {
   }
 
-  kripke_explicit::kripke_explicit(bdd_dict* dict,
+  kripke_explicit::kripke_explicit(bdd_dict_ptr dict,
                                    state_kripke*  init)
     : dict_(dict),
       init_ (init)
@@ -169,7 +169,7 @@ namespace spot
     return init_;
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   kripke_explicit::get_dict() const
   {
     return dict_;
diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh
index 9bf7d08cc..57b03d19a 100644
--- a/src/kripke/kripkeexplicit.hh
+++ b/src/kripke/kripkeexplicit.hh
@@ -114,11 +114,11 @@ namespace spot
   class SPOT_API kripke_explicit : public kripke
   {
   public:
-    kripke_explicit(bdd_dict*);
-    kripke_explicit(bdd_dict*, state_kripke*);
+    kripke_explicit(bdd_dict_ptr);
+    kripke_explicit(bdd_dict_ptr, state_kripke*);
     ~kripke_explicit();
 
-    bdd_dict* get_dict() const;
+    bdd_dict_ptr get_dict() const;
     state_kripke* get_init_state() const;
 
     /// \brief Allow to get an iterator on the state we passed in
@@ -175,7 +175,7 @@ namespace spot
     void add_transition(state_kripke* source,
 			const state_kripke* dest);
 
-    bdd_dict* dict_;
+    bdd_dict_ptr dict_;
     state_kripke* init_;
     std::map<const std::string, state_kripke*> ns_nodes_;
     std::map<const state_kripke*, std::string> sn_nodes_;
diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc
index a2d0b4f9d..99aeb791d 100644
--- a/src/kripke/kripkeprint.cc
+++ b/src/kripke/kripkeprint.cc
@@ -41,7 +41,7 @@ namespace spot
 
       void process_state(const state* s, int, tgba_succ_iterator* si)
       {
-	const bdd_dict* d = aut_->get_dict();
+	const bdd_dict_ptr d = aut_->get_dict();
 	os_ << '"';
 	escape_str(os_, aut_->format_state(s));
 	os_ << "\", \"";
@@ -88,7 +88,7 @@ namespace spot
 	else
 	  notfirst = true;
 
-	const bdd_dict* d = aut_->get_dict();
+	const bdd_dict_ptr d = aut_->get_dict();
 	os_ << 'S' << in_s << ", \"";
 	const kripke* automata = down_cast<const kripke*>(aut_);
 	assert(automata);
diff --git a/src/kripkeparse/kripkeparse.yy b/src/kripkeparse/kripkeparse.yy
index d9df3a058..ae2436ab4 100644
--- a/src/kripkeparse/kripkeparse.yy
+++ b/src/kripkeparse/kripkeparse.yy
@@ -198,7 +198,7 @@ namespace spot
   kripke_explicit*
   kripke_parse(const std::string& name,
                kripke_parse_error_list& error_list,
-               bdd_dict* dict,
+               bdd_dict_ptr dict,
                environment& env,
                bool debug)
   {
diff --git a/src/kripkeparse/public.hh b/src/kripkeparse/public.hh
index 0ce797475..fa8474ac0 100644
--- a/src/kripkeparse/public.hh
+++ b/src/kripkeparse/public.hh
@@ -41,7 +41,7 @@ namespace spot
   SPOT_API kripke_explicit*
   kripke_parse(const std::string& name,
                kripke_parse_error_list& error_list,
-               bdd_dict* dict,
+               bdd_dict_ptr dict,
                ltl::environment& env
                = ltl::default_environment::instance(),
                bool debug = false);
diff --git a/src/kripketest/parse_print_test.cc b/src/kripketest/parse_print_test.cc
index 4c31f0347..905b90cbf 100644
--- a/src/kripketest/parse_print_test.cc
+++ b/src/kripketest/parse_print_test.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2011 Laboratoire de Recherche et Developpement
+// Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
@@ -28,9 +28,8 @@ int main(int argc, char** argv)
 {
   int return_value = 0;
   kripke_parse_error_list pel;
-  bdd_dict* dict = new bdd_dict;
 
-  kripke_explicit* k = kripke_parse(argv[1], pel, dict);
+  kripke_explicit* k = kripke_parse(argv[1], pel, make_bdd_dict());
   if (!pel.empty())
   {
     format_kripke_parse_errors(std::cerr, argv[1], pel);
@@ -41,7 +40,6 @@ int main(int argc, char** argv)
     kripke_save_reachable(std::cout, k);
 
   delete k;
-  delete dict;
   assert(ltl::atomic_prop::instance_count() == 0);
   assert(ltl::unop::instance_count() == 0);
   assert(ltl::binop::instance_count() == 0);
diff --git a/src/ltlvisit/apcollect.cc b/src/ltlvisit/apcollect.cc
index 50d99a615..c0ce810bc 100644
--- a/src/ltlvisit/apcollect.cc
+++ b/src/ltlvisit/apcollect.cc
@@ -76,7 +76,7 @@ namespace spot
     {
       spot::ltl::atomic_prop_set aps;
       atomic_prop_collect(f, &aps);
-      bdd_dict* d = a->get_dict();
+      auto d = a->get_dict();
       bdd res = bddtrue;
       for (atomic_prop_set::const_iterator i = aps.begin();
 	   i != aps.end(); ++i)
diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc
index 85b888f07..81e49cb9b 100644
--- a/src/ltlvisit/contain.cc
+++ b/src/ltlvisit/contain.cc
@@ -37,7 +37,7 @@ namespace spot
   {
 
     language_containment_checker::language_containment_checker
-      (bdd_dict* dict, bool exprop, bool symb_merge,
+      (bdd_dict_ptr dict, bool exprop, bool symb_merge,
        bool branching_postponement, bool fair_loop_approx)
       : dict_(dict), exprop_(exprop), symb_merge_(symb_merge),
       branching_postponement_(branching_postponement),
diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh
index 7376aa6e0..006d9e8ea 100644
--- a/src/ltlvisit/contain.hh
+++ b/src/ltlvisit/contain.hh
@@ -46,7 +46,7 @@ namespace spot
     public:
       /// This class uses spot::ltl_to_tgba_fm to translate LTL
       /// formulae.  See that function for the meaning of these options.
-      language_containment_checker(bdd_dict* dict, bool exprop,
+      language_containment_checker(bdd_dict_ptr dict, bool exprop,
 				   bool symb_merge,
 				   bool branching_postponement,
 				   bool fair_loop_approx);
@@ -72,7 +72,7 @@ namespace spot
       record_* register_formula_(const formula* f);
 
       /* Translation options */
-      bdd_dict* dict_;
+      bdd_dict_ptr dict_;
       bool exprop_;
       bool symb_merge_;
       bool branching_postponement_;
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index b18fc8606..0fb89dd7a 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -51,7 +51,7 @@ namespace spot
       typedef std::pair<const formula*, const formula*> pairf;
       typedef std::map<pairf, bool> syntimpl_cache_t;
     public:
-      bdd_dict* dict;
+      bdd_dict_ptr dict;
       ltl_simplifier_options options;
       language_containment_checker lcc;
 
@@ -130,12 +130,12 @@ namespace spot
 	dict->unregister_all_my_variables(this);
       }
 
-      ltl_simplifier_cache(bdd_dict* d)
+      ltl_simplifier_cache(bdd_dict_ptr d)
 	: dict(d), lcc(d, true, true, false, false)
       {
       }
 
-      ltl_simplifier_cache(bdd_dict* d, const ltl_simplifier_options& opt)
+      ltl_simplifier_cache(bdd_dict_ptr d, const ltl_simplifier_options& opt)
 	: dict(d), options(opt), lcc(d, true, true, false, false)
       {
 	options.containment_checks |= options.containment_checks_stronger;
@@ -4694,43 +4694,20 @@ namespace spot
     /////////////////////////////////////////////////////////////////////
     // ltl_simplifier
 
-    ltl_simplifier::ltl_simplifier(bdd_dict* d)
+    ltl_simplifier::ltl_simplifier(bdd_dict_ptr d)
     {
-      if (!d)
-	{
-	  d = new bdd_dict;
-	  owndict = true;
-	}
-      else
-	{
-	  owndict = false;
-	}
       cache_ = new ltl_simplifier_cache(d);
     }
 
     ltl_simplifier::ltl_simplifier(const ltl_simplifier_options& opt,
-				   bdd_dict* d)
+				   bdd_dict_ptr d)
     {
-      if (!d)
-	{
-	  d = new bdd_dict;
-	  owndict = true;
-	}
-      else
-	{
-	  owndict = false;
-	}
       cache_ = new ltl_simplifier_cache(d, opt);
     }
 
     ltl_simplifier::~ltl_simplifier()
     {
-      bdd_dict* todelete = 0;
-      if (owndict)
-	todelete = cache_->dict;
       delete cache_;
-      // It has to be deleted after the cache.
-      delete todelete;
     }
 
     const formula*
@@ -4794,7 +4771,7 @@ namespace spot
       return cache_->boolean_to_isop(f);
     }
 
-    bdd_dict*
+    bdd_dict_ptr
     ltl_simplifier::get_dict() const
     {
       return cache_->dict;
diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh
index e63389dfa..05ae752c6 100644
--- a/src/ltlvisit/simplify.hh
+++ b/src/ltlvisit/simplify.hh
@@ -1,4 +1,5 @@
-// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -78,8 +79,9 @@ namespace spot
     class SPOT_API ltl_simplifier
     {
     public:
-      ltl_simplifier(bdd_dict* dict = 0);
-      ltl_simplifier(const ltl_simplifier_options& opt, bdd_dict* dict = 0);
+      ltl_simplifier(bdd_dict_ptr dict = make_bdd_dict());
+      ltl_simplifier(const ltl_simplifier_options& opt,
+		     bdd_dict_ptr dict = make_bdd_dict());
       ~ltl_simplifier();
 
       /// Simplify the formula \a f (using options supplied to the
@@ -157,7 +159,7 @@ namespace spot
       void clear_as_bdd_cache();
 
       /// Return the bdd_dict used.
-      bdd_dict* get_dict() const;
+      bdd_dict_ptr get_dict() const;
 
       /// Cached version of spot::ltl::star_normal_form().
       const formula* star_normal_form(const formula* f);
@@ -177,8 +179,6 @@ namespace spot
       // Copy disallowed.
       ltl_simplifier(const ltl_simplifier&) SPOT_DELETED;
       void operator=(const ltl_simplifier&) SPOT_DELETED;
-
-      bool owndict;
     };
   }
 
diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy
index ed4985091..ac5dd958e 100644
--- a/src/neverparse/neverclaimparse.yy
+++ b/src/neverparse/neverclaimparse.yy
@@ -289,7 +289,7 @@ namespace spot
   tgba_digraph*
   neverclaim_parse(const std::string& name,
 		   neverclaim_parse_error_list& error_list,
-		   bdd_dict* dict,
+		   bdd_dict_ptr dict,
 		   environment& env,
 		   bool debug)
   {
diff --git a/src/neverparse/public.hh b/src/neverparse/public.hh
index ba38c85dd..e1960485d 100644
--- a/src/neverparse/public.hh
+++ b/src/neverparse/public.hh
@@ -59,7 +59,7 @@ namespace spot
   neverclaim_parse(const std::string& filename,
 		   neverclaim_parse_error_list&
 		   error_list,
-		   bdd_dict* dict,
+		   bdd_dict_ptr dict,
 		   ltl::environment& env = ltl::default_environment::instance(),
 		   bool debug = false);
 
diff --git a/src/priv/accmap.hh b/src/priv/accmap.hh
index 4e2a30f1f..fa89849bb 100644
--- a/src/priv/accmap.hh
+++ b/src/priv/accmap.hh
@@ -31,7 +31,7 @@ namespace spot
   class acc_mapper_common
   {
   protected:
-    bdd_dict* dict_;
+    bdd_dict_ptr dict_;
     tgba_digraph* aut_;
     ltl::environment& env_;
     bdd neg_;
diff --git a/src/saba/saba.hh b/src/saba/saba.hh
index 5759112f3..a6882279e 100644
--- a/src/saba/saba.hh
+++ b/src/saba/saba.hh
@@ -85,7 +85,7 @@ namespace spot
     /// This is useful when dealing with several automata (which
     /// may use the same BDD variable for different formula),
     /// or simply when printing.
-    virtual bdd_dict* get_dict() const = 0;
+    virtual bdd_dict_ptr get_dict() const = 0;
 
     /// \brief Format the state as a string for printing.
     ///
diff --git a/src/saba/sabacomplementtgba.cc b/src/saba/sabacomplementtgba.cc
index b375475c5..3dba478c6 100644
--- a/src/saba/sabacomplementtgba.cc
+++ b/src/saba/sabacomplementtgba.cc
@@ -415,7 +415,7 @@ namespace spot
                                                   state);
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   saba_complement_tgba::get_dict() const
   {
     return automaton_->get_dict();
diff --git a/src/saba/sabacomplementtgba.hh b/src/saba/sabacomplementtgba.hh
index fbd5343cd..f622eca30 100644
--- a/src/saba/sabacomplementtgba.hh
+++ b/src/saba/sabacomplementtgba.hh
@@ -63,7 +63,7 @@ namespace spot
     virtual saba_succ_iterator*
     succ_iter(const saba_state* local_state) const;
 
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
     virtual std::string format_state(const saba_state* state) const;
     virtual bdd all_acceptance_conditions() const;
   private:
diff --git a/src/sabatest/sabacomplementtgba.cc b/src/sabatest/sabacomplementtgba.cc
index 326253f87..b8198c9c2 100644
--- a/src/sabatest/sabacomplementtgba.cc
+++ b/src/sabatest/sabacomplementtgba.cc
@@ -64,15 +64,12 @@ int main(int argc, char* argv[])
     return 1;
   }
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
-  spot::tgba* a;
-
   spot::ltl::parse_error_list p1;
   const spot::ltl::formula* f1 = spot::ltl::parse(formula, p1);
   if (spot::ltl::format_parse_errors(std::cerr, formula, p1))
     return 2;
 
-  a = spot::ltl_to_tgba_fm(f1, dict);
+  auto a = spot::ltl_to_tgba_fm(f1, spot::make_bdd_dict());
 
   spot::saba_complement_tgba* complement =
     new spot::saba_complement_tgba(a);
@@ -82,5 +79,4 @@ int main(int argc, char* argv[])
   delete complement;
   delete a;
   f1->destroy();
-  delete dict;
 }
diff --git a/src/ta/ta.hh b/src/ta/ta.hh
index a71b7d944..a8b6dde18 100644
--- a/src/ta/ta.hh
+++ b/src/ta/ta.hh
@@ -129,7 +129,7 @@ namespace spot
     /// This is useful when dealing with several automata (which
     /// may use the same BDD variable for different formula),
     /// or simply when printing.
-    virtual bdd_dict*
+    virtual bdd_dict_ptr
     get_dict() const = 0;
 
     /// \brief Format the state as a string for printing.
diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc
index 407b87860..661b2e697 100644
--- a/src/ta/taexplicit.cc
+++ b/src/ta/taexplicit.cc
@@ -490,7 +490,7 @@ namespace spot
     return new ta_explicit_succ_iterator(s, condition);
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   ta_explicit::get_dict() const
   {
     return tgba_->get_dict();
diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh
index 3cb0197aa..421b44e85 100644
--- a/src/ta/taexplicit.hh
+++ b/src/ta/taexplicit.hh
@@ -73,7 +73,7 @@ namespace spot
     virtual ta_succ_iterator*
     succ_iter(const spot::state* s, bdd condition) const;
 
-    virtual bdd_dict*
+    virtual bdd_dict_ptr
     get_dict() const;
 
     virtual std::string
diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc
index f773ae68f..4dcc9411b 100644
--- a/src/ta/taproduct.cc
+++ b/src/ta/taproduct.cc
@@ -328,7 +328,7 @@ namespace spot
 
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   ta_product::get_dict() const
   {
     return dict_;
diff --git a/src/ta/taproduct.hh b/src/ta/taproduct.hh
index 300f0dd2b..fc5f9cad7 100644
--- a/src/ta/taproduct.hh
+++ b/src/ta/taproduct.hh
@@ -150,7 +150,7 @@ namespace spot
     virtual ta_succ_iterator_product*
     succ_iter(const spot::state* s, bdd changeset) const;
 
-    virtual bdd_dict*
+    virtual bdd_dict_ptr
     get_dict() const;
 
     virtual std::string
@@ -192,7 +192,7 @@ namespace spot
     }
 
   private:
-    bdd_dict* dict_;
+    bdd_dict_ptr dict_;
     const ta* ta_;
     const kripke* kripke_;
 
diff --git a/src/ta/tgtaexplicit.cc b/src/ta/tgtaexplicit.cc
index bf99f3017..84a2371dd 100644
--- a/src/ta/tgtaexplicit.cc
+++ b/src/ta/tgtaexplicit.cc
@@ -56,7 +56,7 @@ namespace spot
     return ta_.get_tgba()->support_conditions(s->get_tgba_state());
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgta_explicit::get_dict() const
   {
     return ta_.get_dict();
diff --git a/src/ta/tgtaexplicit.hh b/src/ta/tgtaexplicit.hh
index efb6bb327..7c1c40f71 100644
--- a/src/ta/tgtaexplicit.hh
+++ b/src/ta/tgtaexplicit.hh
@@ -48,7 +48,7 @@ namespace spot
     virtual tgba_succ_iterator*
     succ_iter(const spot::state* local_state) const;
 
-    virtual bdd_dict*
+    virtual bdd_dict_ptr
     get_dict() const;
 
     const ta_explicit* get_ta() const { return &ta_; }
diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc
index 2f9774e90..7010db873 100644
--- a/src/taalgos/dotty.cc
+++ b/src/taalgos/dotty.cc
@@ -97,7 +97,7 @@ namespace spot
       void
       process_link(int in, int out, const ta_succ_iterator* si)
       {
-	bdd_dict* d = t_automata_->get_dict();
+	bdd_dict_ptr d = t_automata_->get_dict();
 	std::string label =
 	  ((in == 1 && artificial_initial_state_)
 	   ? bdd_format_formula(d, si->current_condition())
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index 4c79f33a7..60a85a6f1 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -29,6 +29,7 @@
 #include <iosfwd>
 #include <bdd.h>
 #include <vector>
+#include <memory>
 #include "ltlast/formula.hh"
 
 namespace spot
@@ -227,7 +228,12 @@ namespace spot
     bdd_dict& operator=(const bdd_dict& other) SPOT_DELETED;
   };
 
+  typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
 
+  inline bdd_dict_ptr make_bdd_dict()
+  {
+    return std::make_shared<bdd_dict>();
+  }
 }
 
 #endif // SPOT_TGBA_BDDDICT_HH
diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc
index e796eaf0b..1927d6944 100644
--- a/src/tgba/bddprint.cc
+++ b/src/tgba/bddprint.cc
@@ -31,7 +31,7 @@
 namespace spot
 {
   /// Global dictionary used by print_handler() to lookup variables.
-  static const bdd_dict* dict;
+  static bdd_dict_ptr dict;
 
   /// Global flag to enable Acc[x] output (instead of `x').
   static bool want_acc;
@@ -98,7 +98,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_sat(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_sat(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     dict = d;
     where = &os;
@@ -120,7 +120,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_acc(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_acc(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     dict = d;
     where = &os;
@@ -143,7 +143,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_accset(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_accset(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     dict = d;
     where = &os;
@@ -156,7 +156,7 @@ namespace spot
   }
 
   std::string
-  bdd_format_accset(const bdd_dict* d, bdd b)
+  bdd_format_accset(bdd_dict_ptr d, bdd b)
   {
     std::ostringstream os;
     bdd_print_accset(os, d, b);
@@ -164,7 +164,7 @@ namespace spot
   }
 
   std::string
-  bdd_format_sat(const bdd_dict* d, bdd b)
+  bdd_format_sat(bdd_dict_ptr d, bdd b)
   {
     std::ostringstream os;
     bdd_print_sat(os, d, b);
@@ -172,7 +172,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_set(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_set(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     dict = d;
     want_acc = true;
@@ -183,7 +183,7 @@ namespace spot
   }
 
   std::string
-  bdd_format_set(const bdd_dict* d, bdd b)
+  bdd_format_set(const bdd_dict_ptr d, bdd b)
   {
     std::ostringstream os;
     bdd_print_set(os, d, b);
@@ -191,7 +191,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_formula(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_formula(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     const ltl::formula* f = bdd_to_formula(b, d);
     print_ltl(f, os);
@@ -200,7 +200,7 @@ namespace spot
   }
 
   std::string
-  bdd_format_formula(const bdd_dict* d, bdd b)
+  bdd_format_formula(bdd_dict_ptr d, bdd b)
   {
     std::ostringstream os;
     bdd_print_formula(os, d, b);
@@ -208,7 +208,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_dot(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_dot(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     dict = d;
     want_acc = true;
@@ -219,7 +219,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_table(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_table(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     dict = d;
     want_acc = true;
@@ -236,7 +236,7 @@ namespace spot
   }
 
   std::ostream&
-  bdd_print_isop(std::ostream& os, const bdd_dict* d, bdd b)
+  bdd_print_isop(std::ostream& os, bdd_dict_ptr d, bdd b)
   {
     dict = d;
     want_acc = true;
@@ -252,7 +252,7 @@ namespace spot
   }
 
   std::string
-  bdd_format_isop(const bdd_dict* d, bdd b)
+  bdd_format_isop(bdd_dict_ptr d, bdd b)
   {
     std::ostringstream os;
     bdd_print_isop(os, d, b);
diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh
index 889f4b834..a71bfab31 100644
--- a/src/tgba/bddprint.hh
+++ b/src/tgba/bddprint.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -38,7 +38,7 @@ namespace spot
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   SPOT_API std::ostream&
-  bdd_print_sat(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_sat(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
   /// \brief Format a BDD as a list of literals.
   ///
@@ -47,7 +47,7 @@ namespace spot
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   SPOT_API std::string
-  bdd_format_sat(const bdd_dict* dict, bdd b);
+  bdd_format_sat(bdd_dict_ptr dict, bdd b);
 
   /// \brief Print a BDD as a list of acceptance conditions.
   ///
@@ -57,7 +57,7 @@ namespace spot
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   SPOT_API std::ostream&
-  bdd_print_acc(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_acc(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
   /// \brief Print a BDD as a set of acceptance conditions.
   ///
@@ -67,7 +67,7 @@ namespace spot
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   SPOT_API std::ostream&
-  bdd_print_accset(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_accset(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
   /// \brief Format a BDD as a set of acceptance conditions.
   ///
@@ -76,49 +76,49 @@ namespace spot
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   SPOT_API std::string
-  bdd_format_accset(const bdd_dict* dict, bdd b);
+  bdd_format_accset(bdd_dict_ptr dict, bdd b);
 
   /// \brief Print a BDD as a set.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   SPOT_API std::ostream&
-  bdd_print_set(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_set(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
   /// \brief Format a BDD as a set.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   SPOT_API std::string
-  bdd_format_set(const bdd_dict* dict, bdd b);
+  bdd_format_set(bdd_dict_ptr dict, bdd b);
 
   /// \brief Print a BDD as a formula.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   SPOT_API std::ostream&
-  bdd_print_formula(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_formula(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
   /// \brief Format a BDD as a formula.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   SPOT_API std::string
-  bdd_format_formula(const bdd_dict* dict, bdd b);
+  bdd_format_formula(bdd_dict_ptr dict, bdd b);
 
   /// \brief Print a BDD as a diagram in dotty format.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   SPOT_API std::ostream&
-  bdd_print_dot(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_dot(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
   /// \brief Print a BDD as a table.
   /// \param os The output stream.
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   SPOT_API std::ostream&
-  bdd_print_table(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_table(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
   /// \brief Enable UTF-8 output for bdd printers.
   SPOT_API void enable_utf8();
@@ -129,7 +129,7 @@ namespace spot
   /// \param b The BDD to print.
   /// \return The BDD formated as a string.
   SPOT_API std::string
-  bdd_format_isop(const bdd_dict* dict, bdd b);
+  bdd_format_isop(bdd_dict_ptr dict, bdd b);
 
 
   /// \brief Print a BDD as an irredundant sum of product.
@@ -137,7 +137,7 @@ namespace spot
   /// \param dict The dictionary to use, to lookup variables.
   /// \param b The BDD to print.
   SPOT_API std::ostream&
-  bdd_print_isop(std::ostream& os, const bdd_dict* dict, bdd b);
+  bdd_print_isop(std::ostream& os, bdd_dict_ptr dict, bdd b);
 
 }
 
diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc
index 0a2845286..4f3648941 100644
--- a/src/tgba/formula2bdd.cc
+++ b/src/tgba/formula2bdd.cc
@@ -35,7 +35,7 @@ namespace spot
     class formula_to_bdd_visitor: public ltl::visitor
     {
     public:
-      formula_to_bdd_visitor(bdd_dict* d, void* owner)
+      formula_to_bdd_visitor(bdd_dict_ptr d, void* owner)
 	: d_(d), owner_(owner)
       {
       }
@@ -167,14 +167,14 @@ namespace spot
       }
 
     private:
-      bdd_dict* d_;
+      bdd_dict_ptr d_;
       void* owner_;
       bdd res_;
     };
 
     // Convert a BDD which is known to be a conjonction into a formula.
     static const ltl::formula*
-    conj_to_formula(bdd b, const bdd_dict* d)
+    conj_to_formula(bdd b, const bdd_dict_ptr d)
     {
       if (b == bddfalse)
 	return constant::false_instance();
@@ -207,7 +207,7 @@ namespace spot
   } // anonymous
 
   bdd
-  formula_to_bdd(const formula* f, bdd_dict* d, void* for_me)
+  formula_to_bdd(const formula* f, bdd_dict_ptr d, void* for_me)
   {
     formula_to_bdd_visitor v(d, for_me);
     f->accept(v);
@@ -215,7 +215,7 @@ namespace spot
   }
 
   const formula*
-  bdd_to_formula(bdd f, const bdd_dict* d)
+  bdd_to_formula(bdd f, const bdd_dict_ptr d)
   {
     if (f == bddfalse)
       return constant::false_instance();
diff --git a/src/tgba/formula2bdd.hh b/src/tgba/formula2bdd.hh
index f8820fb9b..1525639e5 100644
--- a/src/tgba/formula2bdd.hh
+++ b/src/tgba/formula2bdd.hh
@@ -39,7 +39,7 @@ namespace spot
   /// to unregister the variables that have been registered for \a
   /// for_me.  See bdd_dict::unregister_all_my_variables().
   SPOT_API bdd
-  formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me);
+  formula_to_bdd(const ltl::formula* f, bdd_dict_ptr d, void* for_me);
 
   /// \brief Convert a BDD into a formula.
   ///
@@ -50,7 +50,7 @@ namespace spot
   /// been registered in \a d.  Although the result has type
   /// ltl::formula*, it obviously does not use any temporal operator.
   SPOT_API const
-  ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d);
+  ltl::formula* bdd_to_formula(bdd f, const bdd_dict_ptr d);
 }
 
 #endif // SPOT_TGBA_FORMULA2BDD_HH
diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc
index 45bbc1c3f..c0b554520 100644
--- a/src/tgba/taatgba.cc
+++ b/src/tgba/taatgba.cc
@@ -33,7 +33,7 @@ namespace spot
   | taa_tgba |
   `--------*/
 
-  taa_tgba::taa_tgba(bdd_dict* dict)
+  taa_tgba::taa_tgba(bdd_dict_ptr dict)
     : dict_(dict),
       all_acceptance_conditions_(bddfalse),
       all_acceptance_conditions_computed_(false),
@@ -72,7 +72,7 @@ namespace spot
     return new taa_succ_iterator(s->get_state(), all_acceptance_conditions());
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   taa_tgba::get_dict() const
   {
     return dict_;
diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh
index 75ffe0fd8..2368c2cec 100644
--- a/src/tgba/taatgba.hh
+++ b/src/tgba/taatgba.hh
@@ -35,7 +35,7 @@ namespace spot
   class SPOT_API taa_tgba : public tgba
   {
   public:
-    taa_tgba(bdd_dict* dict);
+    taa_tgba(bdd_dict_ptr dict);
 
     struct transition;
     typedef std::list<transition*> state;
@@ -55,7 +55,7 @@ namespace spot
     virtual ~taa_tgba();
     virtual spot::state* get_init_state() const;
     virtual tgba_succ_iterator* succ_iter(const spot::state* state) const;
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
     virtual std::string format_state(const spot::state* state) const = 0;
     virtual bdd all_acceptance_conditions() const;
     virtual bdd neg_acceptance_conditions() const;
@@ -65,7 +65,7 @@ namespace spot
 
     typedef std::vector<taa_tgba::state_set*> ss_vec;
 
-    bdd_dict* dict_;
+    bdd_dict_ptr dict_;
     mutable bdd all_acceptance_conditions_;
     mutable bool all_acceptance_conditions_computed_;
     bdd neg_acceptance_conditions_;
@@ -151,7 +151,7 @@ namespace spot
   class SPOT_API taa_tgba_labelled : public taa_tgba
   {
   public:
-    taa_tgba_labelled(bdd_dict* dict) : taa_tgba(dict) {};
+    taa_tgba_labelled(bdd_dict_ptr dict) : taa_tgba(dict) {};
 
     void set_init_state(const label& s)
     {
@@ -322,7 +322,7 @@ namespace spot
     public taa_tgba_labelled<std::string, string_hash>
   {
   public:
-    taa_tgba_string(bdd_dict* dict) :
+    taa_tgba_string(bdd_dict_ptr dict) :
       taa_tgba_labelled<std::string, string_hash>(dict) {};
     ~taa_tgba_string();
   protected:
@@ -334,7 +334,7 @@ namespace spot
     public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>
   {
   public:
-    taa_tgba_formula(bdd_dict* dict) :
+    taa_tgba_formula(bdd_dict_ptr dict) :
       taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict) {};
     ~taa_tgba_formula();
   protected:
diff --git a/src/tgba/tgba.hh b/src/tgba/tgba.hh
index 4f3d07f45..7a719befe 100644
--- a/src/tgba/tgba.hh
+++ b/src/tgba/tgba.hh
@@ -175,7 +175,7 @@ namespace spot
     /// formulae, and vice versa.  This is useful when dealing with
     /// several automata (which may use the same BDD variable for
     /// different formula), or simply when printing.
-    virtual bdd_dict* get_dict() const = 0;
+    virtual bdd_dict_ptr get_dict() const = 0;
 
     /// \brief Format the state as a string for printing.
     ///
diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index c8e87a168..b2c4d25ab 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -160,13 +160,13 @@ namespace spot
 
   protected:
     graph_t g_;
-    bdd_dict* dict_;
+    bdd_dict_ptr dict_;
     bdd all_acceptance_conditions_;
     bdd neg_acceptance_conditions_;
     mutable unsigned init_number_;
 
   public:
-    tgba_digraph(bdd_dict* dict)
+    tgba_digraph(bdd_dict_ptr dict)
       : dict_(dict),
 	all_acceptance_conditions_(bddfalse),
 	neg_acceptance_conditions_(bddtrue),
@@ -211,7 +211,7 @@ namespace spot
       return g_;
     }
 
-    virtual bdd_dict* get_dict() const
+    virtual bdd_dict_ptr get_dict() const
     {
       return this->dict_;
     }
diff --git a/src/tgba/tgbakvcomplement.cc b/src/tgba/tgbakvcomplement.cc
index 7ab10b56e..cd1949681 100644
--- a/src/tgba/tgbakvcomplement.cc
+++ b/src/tgba/tgbakvcomplement.cc
@@ -627,7 +627,7 @@ namespace spot
 						acc_list_, s);
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgba_kv_complement::get_dict() const
   {
     return automaton_->get_dict();
diff --git a/src/tgba/tgbakvcomplement.hh b/src/tgba/tgbakvcomplement.hh
index 60959c6b7..4605f814c 100644
--- a/src/tgba/tgbakvcomplement.hh
+++ b/src/tgba/tgbakvcomplement.hh
@@ -93,7 +93,7 @@ namespace spot
     virtual state* get_init_state() const;
     virtual tgba_succ_iterator* succ_iter(const state* state) const;
 
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
     virtual std::string format_state(const state* state) const;
     virtual bdd all_acceptance_conditions() const;
     virtual bdd neg_acceptance_conditions() const;
diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc
index f22268393..42563de10 100644
--- a/src/tgba/tgbaproduct.cc
+++ b/src/tgba/tgbaproduct.cc
@@ -411,7 +411,7 @@ namespace spot
     return lsc & rsc;
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgba_product::get_dict() const
   {
     return dict_;
diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh
index fea330cf1..e15baba6c 100644
--- a/src/tgba/tgbaproduct.hh
+++ b/src/tgba/tgbaproduct.hh
@@ -94,7 +94,7 @@ namespace spot
     virtual tgba_succ_iterator*
     succ_iter(const state* state) const;
 
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
 
     virtual std::string format_state(const state* state) const;
 
@@ -110,7 +110,7 @@ namespace spot
     virtual bdd compute_support_conditions(const state* state) const;
 
   protected:
-    bdd_dict* dict_;
+    bdd_dict_ptr dict_;
     const tgba* left_;
     const tgba* right_;
     bool left_kripke_;
diff --git a/src/tgba/tgbaproxy.cc b/src/tgba/tgbaproxy.cc
index 499fded5c..79a33dc27 100644
--- a/src/tgba/tgbaproxy.cc
+++ b/src/tgba/tgbaproxy.cc
@@ -48,7 +48,7 @@ namespace spot
     return original_->succ_iter(state);
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgba_proxy::get_dict() const
   {
     return original_->get_dict();
diff --git a/src/tgba/tgbaproxy.hh b/src/tgba/tgbaproxy.hh
index c076cef17..9aa5162d1 100644
--- a/src/tgba/tgbaproxy.hh
+++ b/src/tgba/tgbaproxy.hh
@@ -46,7 +46,7 @@ namespace spot
     virtual tgba_succ_iterator*
     succ_iter(const state* state) const;
 
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
 
     virtual std::string format_state(const state* state) const;
 
diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc
index d72f3d282..6b74b5b9d 100644
--- a/src/tgba/tgbasafracomplement.cc
+++ b/src/tgba/tgbasafracomplement.cc
@@ -1249,7 +1249,7 @@ namespace spot
     return new tgba_safra_complement_succ_iterator(succ_list, condition);
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgba_safra_complement::get_dict() const
   {
     return automaton_->get_dict();
diff --git a/src/tgba/tgbasafracomplement.hh b/src/tgba/tgbasafracomplement.hh
index ffad857ea..95ab2a89b 100644
--- a/src/tgba/tgbasafracomplement.hh
+++ b/src/tgba/tgbasafracomplement.hh
@@ -57,7 +57,7 @@ namespace spot
     virtual state* get_init_state() const;
     virtual tgba_succ_iterator* succ_iter(const state* state) const;
 
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
     virtual std::string format_state(const state* state) const;
     virtual bdd all_acceptance_conditions() const;
     virtual bdd neg_acceptance_conditions() const;
diff --git a/src/tgba/tgbascc.cc b/src/tgba/tgbascc.cc
index 662d6d7e7..a5da1fb7f 100644
--- a/src/tgba/tgbascc.cc
+++ b/src/tgba/tgbascc.cc
@@ -56,7 +56,7 @@ namespace spot
     return aut_->succ_iter(state);
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgba_scc::get_dict() const
   {
     return aut_->get_dict();
diff --git a/src/tgba/tgbascc.hh b/src/tgba/tgbascc.hh
index 28f45f30e..0dcae06f4 100644
--- a/src/tgba/tgbascc.hh
+++ b/src/tgba/tgbascc.hh
@@ -58,7 +58,7 @@ namespace spot
 
     virtual state* get_init_state() const;
     virtual tgba_succ_iterator* succ_iter(const state* state) const;
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
 
     virtual std::string
     transition_annotation(const tgba_succ_iterator* t) const;
diff --git a/src/tgba/tgbasgba.cc b/src/tgba/tgbasgba.cc
index 45b52c117..501c56d06 100644
--- a/src/tgba/tgbasgba.cc
+++ b/src/tgba/tgbasgba.cc
@@ -199,7 +199,7 @@ namespace spot
     return new tgba_sgba_proxy_succ_iterator(it);
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgba_sgba_proxy::get_dict() const
   {
     return a_->get_dict();
diff --git a/src/tgba/tgbasgba.hh b/src/tgba/tgbasgba.hh
index fecb77da2..6244251e7 100644
--- a/src/tgba/tgbasgba.hh
+++ b/src/tgba/tgbasgba.hh
@@ -44,7 +44,7 @@ namespace spot
 
     virtual tgba_succ_iterator* succ_iter(const state* state) const;
 
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
 
     virtual std::string format_state(const state* state) const;
 
diff --git a/src/tgba/tgbaunion.cc b/src/tgba/tgbaunion.cc
index 89409c047..8567ee76d 100644
--- a/src/tgba/tgbaunion.cc
+++ b/src/tgba/tgbaunion.cc
@@ -372,7 +372,7 @@ namespace spot
       return right_->support_conditions(s->right());
   }
 
-  bdd_dict*
+  bdd_dict_ptr
   tgba_union::get_dict() const
   {
     return dict_;
diff --git a/src/tgba/tgbaunion.hh b/src/tgba/tgbaunion.hh
index fab451928..6c67c1b32 100644
--- a/src/tgba/tgbaunion.hh
+++ b/src/tgba/tgbaunion.hh
@@ -126,7 +126,7 @@ namespace spot
     virtual tgba_succ_iterator_union*
     succ_iter(const state* state) const;
 
-    virtual bdd_dict* get_dict() const;
+    virtual bdd_dict_ptr get_dict() const;
 
     virtual std::string format_state(const state* state) const;
 
@@ -139,7 +139,7 @@ namespace spot
     virtual bdd compute_support_conditions(const state* state) const;
 
   private:
-    bdd_dict* dict_;
+    bdd_dict_ptr dict_;
     const tgba* left_;
     const tgba* right_;
     bdd left_acc_missing_;
diff --git a/src/tgba/wdbacomp.cc b/src/tgba/wdbacomp.cc
index 8642dcd9e..b61b98e9f 100644
--- a/src/tgba/wdbacomp.cc
+++ b/src/tgba/wdbacomp.cc
@@ -227,7 +227,7 @@ namespace spot
 	return new tgba_wdba_comp_proxy_succ_iterator(it, the_acceptance_cond_);
       }
 
-      virtual bdd_dict*
+      virtual bdd_dict_ptr
       get_dict() const
       {
 	return a_->get_dict();
diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc
index b74806380..43eb76caf 100644
--- a/src/tgbaalgos/compsusp.cc
+++ b/src/tgbaalgos/compsusp.cc
@@ -215,7 +215,7 @@ namespace spot
     tgba_digraph*
     susp_prod(tgba* left, const ltl::formula* f, bdd v)
     {
-      bdd_dict* dict = left->get_dict();
+      bdd_dict_ptr dict = left->get_dict();
       const tgba_digraph* a1 = ltl_to_tgba_fm(f, dict, true, true);
 
       const tgba_digraph* a2 = scc_filter(a1, false);
@@ -350,7 +350,7 @@ namespace spot
 
 
   tgba_digraph*
-  compsusp(const ltl::formula* f, bdd_dict* dict,
+  compsusp(const ltl::formula* f, bdd_dict_ptr dict,
 	   bool no_wdba, bool no_simulation,
 	   bool early_susp, bool no_susp_product, bool wdba_smaller,
 	   bool oblig)
diff --git a/src/tgbaalgos/compsusp.hh b/src/tgbaalgos/compsusp.hh
index d8c3fb3c6..28a43d687 100644
--- a/src/tgbaalgos/compsusp.hh
+++ b/src/tgbaalgos/compsusp.hh
@@ -51,7 +51,7 @@ namespace spot
   /// long-term stability should better use the services of the
   /// spot::translator class instead.
   SPOT_API tgba_digraph*
-  compsusp(const ltl::formula* f, bdd_dict* dict,
+  compsusp(const ltl::formula* f, bdd_dict_ptr dict,
 	   bool no_wdba = false, bool no_simulation = false,
 	   bool early_susp = false, bool no_susp_product = false,
 	   bool wdba_smaller = false, bool oblig = false);
diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc
index ae65282a4..b47e82586 100644
--- a/src/tgbaalgos/degen.cc
+++ b/src/tgbaalgos/degen.cc
@@ -208,7 +208,7 @@ namespace spot
       }
 
       void
-      print(int scc, const bdd_dict* dict)
+      print(int scc, const bdd_dict_ptr dict)
       {
         std::vector<bdd>::iterator i;
         std::cout << "Order_" << scc << ":\t";
@@ -241,7 +241,7 @@ namespace spot
       }
 
       void
-      print(const bdd_dict* dict)
+      print(const bdd_dict_ptr dict)
       {
         std::map<int, acc_order>::iterator i;
         for (i = orders_.begin(); i != orders_.end(); i++)
@@ -256,7 +256,7 @@ namespace spot
     {
       bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;
 
-      bdd_dict* dict = a->get_dict();
+      bdd_dict_ptr dict = a->get_dict();
 
       // The result automaton is an SBA.
       auto res = new tgba_digraph(dict);
diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index 14e0cde5b..3217733b5 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -53,7 +53,7 @@ namespace spot
 {
   namespace
   {
-    static bdd_dict* debug_dict = 0;
+    static bdd_dict_ptr debug_dict;
 
     struct transition
     {
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index b8ed4c9ab..3b7984a35 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -56,7 +56,7 @@ namespace spot
 {
   namespace
   {
-    static bdd_dict* debug_dict = 0;
+    static bdd_dict_ptr debug_dict = 0;
 
     struct transition
     {
@@ -303,7 +303,7 @@ namespace spot
       {
 	d.nvars = 0;
 
-	bdd_dict* bd = aut->get_dict();
+	bdd_dict_ptr bd = aut->get_dict();
 	ltl::default_environment& env = ltl::default_environment::instance();
 
 	d.cand_acc.resize(d.cand_nacc);
diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc
index e4f93cb95..9898790cf 100644
--- a/src/tgbaalgos/emptiness.cc
+++ b/src/tgbaalgos/emptiness.cc
@@ -80,7 +80,7 @@ namespace spot
 		 const tgba* a,
 		 const tgba_run* run)
   {
-    bdd_dict* d = a->get_dict();
+    bdd_dict_ptr d = a->get_dict();
     os << "Prefix:" << std::endl;
     for (tgba_run::steps::const_iterator i = run->prefix.begin();
 	 i != run->prefix.end(); ++i)
diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc
index 3a4ce30ef..68ac22251 100644
--- a/src/tgbaalgos/lbtt.cc
+++ b/src/tgbaalgos/lbtt.cc
@@ -173,7 +173,7 @@ namespace spot
     const tgba_digraph*
     lbtt_read_tgba(unsigned num_states, unsigned num_acc,
 		   std::istream& is, std::string& error,
-		   bdd_dict* dict,
+		   bdd_dict_ptr dict,
 		   ltl::environment& env, ltl::environment& envacc)
     {
       auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict));
@@ -238,7 +238,7 @@ namespace spot
     const tgba_digraph*
     lbtt_read_gba(unsigned num_states, unsigned num_acc,
 		  std::istream& is, std::string& error,
-		  bdd_dict* dict,
+		  bdd_dict_ptr dict,
 		  ltl::environment& env, ltl::environment& envacc)
     {
       auto aut = std::unique_ptr<tgba_digraph>(new tgba_digraph(dict));
@@ -314,7 +314,7 @@ namespace spot
 
 
   const tgba_digraph*
-  lbtt_parse(std::istream& is, std::string& error, bdd_dict* dict,
+  lbtt_parse(std::istream& is, std::string& error, bdd_dict_ptr dict,
 	     ltl::environment& env, ltl::environment& envacc)
   {
     is >> std::skipws;
diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh
index fe8e3a3a6..ed91234c6 100644
--- a/src/tgbaalgos/lbtt.hh
+++ b/src/tgbaalgos/lbtt.hh
@@ -53,7 +53,7 @@ namespace spot
   /// \return the read tgba or 0 on error.
   SPOT_API const tgba_digraph*
   lbtt_parse(std::istream& is, std::string& error,
-	     bdd_dict* dict,
+	     bdd_dict_ptr dict,
 	     ltl::environment& env = ltl::default_environment::instance(),
 	     ltl::environment& envacc = ltl::default_environment::instance());
 }
diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc
index 56f940b99..f39be7513 100644
--- a/src/tgbaalgos/ltl2taa.cc
+++ b/src/tgbaalgos/ltl2taa.cc
@@ -418,7 +418,7 @@ namespace spot
   } // anonymous
 
   taa_tgba*
-  ltl_to_taa(const ltl::formula* f, bdd_dict* dict, bool refined_rules)
+  ltl_to_taa(const ltl::formula* f, bdd_dict_ptr dict, bool refined_rules)
   {
     // TODO: s/unabbreviate_ltl/unabbreviate_logic/
     const ltl::formula* f1 = ltl::unabbreviate_ltl(f);
@@ -426,9 +426,9 @@ namespace spot
     f1->destroy();
 
     spot::taa_tgba_formula* res = new spot::taa_tgba_formula(dict);
-    bdd_dict b;
     language_containment_checker* lcc =
-      new language_containment_checker(&b, false, false, false, false);
+      new language_containment_checker(make_bdd_dict(),
+				       false, false, false, false);
     ltl2taa_visitor v(res, lcc, refined_rules);
     f2->accept(v);
     taa_tgba* taa = v.result(); // Careful: before the destroy!
diff --git a/src/tgbaalgos/ltl2taa.hh b/src/tgbaalgos/ltl2taa.hh
index 40f4e1f57..75e22c350 100644
--- a/src/tgbaalgos/ltl2taa.hh
+++ b/src/tgbaalgos/ltl2taa.hh
@@ -49,7 +49,7 @@ namespace spot
   /// \param refined_rules If this parameter is set, refined rules are used.
   /// \return A spot::taa that recognizes the language of \a f.
   SPOT_API taa_tgba*
-  ltl_to_taa(const ltl::formula* f, bdd_dict* dict,
+  ltl_to_taa(const ltl::formula* f, bdd_dict_ptr dict,
 	     bool refined_rules = false);
 }
 
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index de60ca8e2..e295df1ad 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -141,7 +141,7 @@ namespace spot
     {
     public:
 
-      translate_dict(bdd_dict* dict, ltl_simplifier* ls, bool exprop,
+      translate_dict(bdd_dict_ptr dict, ltl_simplifier* ls, bool exprop,
 		     bool single_acc)
 	: dict(dict),
 	  ls(ls),
@@ -167,7 +167,7 @@ namespace spot
 	  j++->first.f->destroy();
       }
 
-      bdd_dict* dict;
+      bdd_dict_ptr dict;
       ltl_simplifier* ls;
       mark_tools mt;
 
@@ -2029,7 +2029,7 @@ namespace spot
 
 
   tgba_digraph*
-  ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
+  ltl_to_tgba_fm(const formula* f, bdd_dict_ptr dict,
 		 bool exprop, bool symb_merge, bool branching_postponement,
 		 bool fair_loop_approx, const atomic_prop_set* unobs,
 		 ltl_simplifier* simplifier)
diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh
index 829429827..a5df0ffae 100644
--- a/src/tgbaalgos/ltl2tgba_fm.hh
+++ b/src/tgbaalgos/ltl2tgba_fm.hh
@@ -123,7 +123,7 @@ namespace spot
   ///
   /// \return A spot::tgba_digraph that recognizes the language of \a f.
   SPOT_API tgba_digraph*
-  ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict,
+  ltl_to_tgba_fm(const ltl::formula* f, bdd_dict_ptr dict,
 		 bool exprop = false, bool symb_merge = true,
 		 bool branching_postponement = false,
 		 bool fair_loop_approx = false,
diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc
index b12312ad2..385840e6a 100644
--- a/src/tgbaalgos/randomgraph.cc
+++ b/src/tgbaalgos/randomgraph.cc
@@ -82,7 +82,7 @@ namespace spot
 
   tgba*
   random_graph(int n, float d,
-	       const ltl::atomic_prop_set* ap, bdd_dict* dict,
+	       const ltl::atomic_prop_set* ap, bdd_dict_ptr dict,
 	       int n_acc, float a, float t,
 	       ltl::environment* env)
   {
diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh
index a92c2e527..ae8111d4a 100644
--- a/src/tgbaalgos/randomgraph.hh
+++ b/src/tgbaalgos/randomgraph.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement de
-// l'Epita (LRDE).
+// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -25,10 +25,10 @@
 
 #include "ltlvisit/apcollect.hh"
 #include "ltlenv/defaultenv.hh"
+#include "tgba/bdddict.hh"
 
 namespace spot
 {
-  class bdd_dict;
   class tgba;
 
   /// \ingroup tgba_misc
@@ -80,7 +80,7 @@ namespace spot
   /// successors one by one.)
   SPOT_API tgba*
   random_graph(int n, float d,
-	       const ltl::atomic_prop_set* ap, bdd_dict* dict,
+	       const ltl::atomic_prop_set* ap, bdd_dict_ptr dict,
 	       int n_acc = 0, float a = 0.1, float t = 0.5,
 	       ltl::environment* env = &ltl::default_environment::instance());
 }
diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc
index 9afd34c8c..fc1ac9d4c 100644
--- a/src/tgbaalgos/save.cc
+++ b/src/tgbaalgos/save.cc
@@ -50,7 +50,7 @@ namespace spot
       void
       process_state(const state* s, int, tgba_succ_iterator* si)
       {
-	const bdd_dict* d = aut_->get_dict();
+	const bdd_dict_ptr d = aut_->get_dict();
 	std::string cur = escape_str(aut_->format_state(s));
 	if (si->first())
 	  do
@@ -73,7 +73,7 @@ namespace spot
       std::ostream&
       print_acc(bdd acc)
       {
-	const bdd_dict* d = aut_->get_dict();
+	const bdd_dict_ptr d = aut_->get_dict();
 	while (acc != bddfalse)
 	  {
 	    bdd cube = bdd_satone(acc);
diff --git a/src/tgbaalgos/translate.cc b/src/tgbaalgos/translate.cc
index fabfaa17f..afbf6f2de 100644
--- a/src/tgbaalgos/translate.cc
+++ b/src/tgbaalgos/translate.cc
@@ -41,7 +41,7 @@ namespace spot
       }
   }
 
-  void translator::build_simplifier(bdd_dict* dict)
+  void translator::build_simplifier(bdd_dict_ptr dict)
   {
     ltl::ltl_simplifier_options options(false, false, false);
     switch (level_)
diff --git a/src/tgbaalgos/translate.hh b/src/tgbaalgos/translate.hh
index 6d9dbd09d..2eb6ca16f 100644
--- a/src/tgbaalgos/translate.hh
+++ b/src/tgbaalgos/translate.hh
@@ -55,7 +55,7 @@ namespace spot
       setup_opt(opt);
     }
 
-    translator(bdd_dict* dict, const option_map* opt = 0)
+    translator(bdd_dict_ptr dict, const option_map* opt = 0)
       : postprocessor(opt)
     {
       build_simplifier(dict);
@@ -65,7 +65,7 @@ namespace spot
     translator(const option_map* opt = 0)
       : postprocessor(opt)
     {
-      build_simplifier(0);
+      build_simplifier(make_bdd_dict());
       setup_opt(opt);
     }
 
@@ -114,7 +114,7 @@ namespace spot
 
   protected:
     void setup_opt(const option_map* opt);
-    void build_simplifier(bdd_dict* dict);
+    void build_simplifier(bdd_dict_ptr dict);
 
   private:
     ltl::ltl_simplifier* simpl_;
diff --git a/src/tgbaalgos/word.cc b/src/tgbaalgos/word.cc
index ad5d6e614..8ae2ed502 100644
--- a/src/tgbaalgos/word.cc
+++ b/src/tgbaalgos/word.cc
@@ -84,7 +84,7 @@ namespace spot
   }
 
   std::ostream&
-  tgba_word::print(std::ostream& os, bdd_dict* d) const
+  tgba_word::print(std::ostream& os, bdd_dict_ptr d) const
   {
     if (!prefix.empty())
       for (seq_t::const_iterator i = prefix.begin(); i != prefix.end(); ++i)
diff --git a/src/tgbaalgos/word.hh b/src/tgbaalgos/word.hh
index af3f5f51e..b463a73db 100644
--- a/src/tgbaalgos/word.hh
+++ b/src/tgbaalgos/word.hh
@@ -31,7 +31,7 @@ namespace spot
   {
     tgba_word(const tgba_run* run);
     void simplify();
-    std::ostream& print(std::ostream& os, bdd_dict* d) const;
+    std::ostream& print(std::ostream& os, bdd_dict_ptr d) const;
 
     typedef std::list<bdd> seq_t;
     seq_t prefix;
diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh
index b8953f8d7..fd62396f4 100644
--- a/src/tgbaparse/public.hh
+++ b/src/tgbaparse/public.hh
@@ -68,7 +68,7 @@ namespace spot
   SPOT_API
   tgba_digraph* tgba_parse(const std::string& filename,
 			   tgba_parse_error_list& error_list,
-			   bdd_dict* dict,
+			   bdd_dict_ptr dict,
 			   ltl::environment& env
 			   = ltl::default_environment::instance(),
 			   ltl::environment& envacc
diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy
index b284ec157..fbd33bf02 100644
--- a/src/tgbaparse/tgbaparse.yy
+++ b/src/tgbaparse/tgbaparse.yy
@@ -219,7 +219,7 @@ namespace spot
   tgba_digraph*
   tgba_parse(const std::string& name,
 	     tgba_parse_error_list& error_list,
-	     bdd_dict* dict,
+	     bdd_dict_ptr dict,
 	     environment& env,
 	     environment& envacc,
 	     bool debug)
diff --git a/src/tgbatest/complementation.cc b/src/tgbatest/complementation.cc
index 44f8c4677..664e76d63 100644
--- a/src/tgbatest/complementation.cc
+++ b/src/tgbatest/complementation.cc
@@ -125,7 +125,7 @@ int main(int argc, char* argv[])
     return 1;
   }
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
   if (print_automaton || print_safra)
   {
     spot::ltl::environment& env(spot::ltl::default_environment::instance());
@@ -318,7 +318,5 @@ int main(int argc, char* argv[])
 
   }
 
-  delete dict;
-
   return return_value;
 }
diff --git a/src/tgbatest/explprod.cc b/src/tgbatest/explprod.cc
index 0215bfcbc..e47791b83 100644
--- a/src/tgbatest/explprod.cc
+++ b/src/tgbatest/explprod.cc
@@ -43,7 +43,7 @@ main(int argc, char** argv)
   if (argc != 3)
     syntax(argv[0]);
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::tgba_parse_error_list pel1;
@@ -67,6 +67,5 @@ main(int argc, char** argv)
   delete a1;
   delete a2;
   assert(spot::ltl::atomic_prop::instance_count() == 0);
-  delete dict;
   return exit_code;
 }
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index c1c88ebe8..949177594 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -381,7 +381,7 @@ main(int argc, char** argv)
   spot::ltl::atomic_prop_set* unobservables = 0;
   spot::tgba* system_aut = 0;
   const spot::tgba* product_to_free = 0;
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
   spot::timer_map tm;
   bool use_timer = false;
   bool reduction_dir_sim = false;
@@ -1018,7 +1018,6 @@ main(int argc, char** argv)
 		  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
 		    {
 		      delete to_free;
-		      delete dict;
 		      return 2;
 		    }
 		  e->merge_transitions();
@@ -1035,7 +1034,6 @@ main(int argc, char** argv)
 		if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
 		  {
 		    delete to_free;
-		    delete dict;
 		    return 2;
 		  }
 		assume_sba = true;
@@ -1053,7 +1051,6 @@ main(int argc, char** argv)
 		    if (!*f)
 		      {
 			std::cerr << "cannot open " << input << std::endl;
-			delete dict;
 			return 2;
 		      }
 		  }
@@ -1067,7 +1064,6 @@ main(int argc, char** argv)
 		if (!to_free)
 		  {
 		    std::cerr << error << std::endl;
-		    delete dict;
 		    return 2;
 		  }
 	      }
@@ -1083,7 +1079,6 @@ main(int argc, char** argv)
 		if (spot::format_dstar_parse_errors(std::cerr, input, pel))
 		  {
 		    delete to_free;
-		    delete dict;
 		    return 2;
 		  }
 		tm.start("dstar2tgba");
@@ -1978,6 +1973,5 @@ main(int argc, char** argv)
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
   assert(spot::ltl::multop::instance_count() == 0);
-  delete dict;
   return exit_code;
 }
diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc
index 0b6331008..a16b405d8 100644
--- a/src/tgbatest/ltlprod.cc
+++ b/src/tgbatest/ltlprod.cc
@@ -58,7 +58,7 @@ main(int argc, char** argv)
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2))
     return 2;
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
   {
     auto a1 = spot::ltl_to_tgba_fm(f1, dict);
     auto a2 = spot::ltl_to_tgba_fm(f2, dict);
@@ -75,6 +75,5 @@ main(int argc, char** argv)
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
   assert(spot::ltl::multop::instance_count() == 0);
-  delete dict;
   return exit_code;
 }
diff --git a/src/tgbatest/maskacc.cc b/src/tgbatest/maskacc.cc
index 9f9f92581..2bc0e29ed 100755
--- a/src/tgbatest/maskacc.cc
+++ b/src/tgbatest/maskacc.cc
@@ -40,7 +40,7 @@ main(int argc, char** argv)
   if (argc != 2)
     syntax(argv[0]);
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::tgba_parse_error_list pel;
@@ -65,6 +65,5 @@ main(int argc, char** argv)
   assert(spot::ltl::atomic_prop::instance_count() != 0);
   delete aut;
   assert(spot::ltl::atomic_prop::instance_count() == 0);
-  delete dict;
   return exit_code;
 }
diff --git a/src/tgbatest/powerset.cc b/src/tgbatest/powerset.cc
index 667c4f6f5..90bc490d4 100644
--- a/src/tgbatest/powerset.cc
+++ b/src/tgbatest/powerset.cc
@@ -44,7 +44,7 @@ main(int argc, char** argv)
   if (argc != 2)
     syntax(argv[0]);
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::tgba_parse_error_list pel;
@@ -67,6 +67,5 @@ main(int argc, char** argv)
   assert(spot::ltl::atomic_prop::instance_count() != 0);
   delete a;
   assert(spot::ltl::atomic_prop::instance_count() == 0);
-  delete dict;
   return exit_code;
 }
diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc
index 7f8de3055..e1b8c0e47 100644
--- a/src/tgbatest/randtgba.cc
+++ b/src/tgbatest/randtgba.cc
@@ -585,7 +585,7 @@ main(int argc, char** argv)
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
 
   spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true);
   spot::ltl::ltl_simplifier simp(simpopt);
@@ -1322,6 +1322,5 @@ main(int argc, char** argv)
 
   delete ap;
   delete apf;
-  delete dict;
   return exit_code;
 }
diff --git a/src/tgbatest/taatgba.cc b/src/tgbatest/taatgba.cc
index 62dedadc8..120cf8cc7 100644
--- a/src/tgbatest/taatgba.cc
+++ b/src/tgbatest/taatgba.cc
@@ -1,4 +1,5 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// -*- coding: utf-8 -*-
+// Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -27,11 +28,9 @@
 int
 main()
 {
-  spot::bdd_dict* dict = new spot::bdd_dict();
-
   spot::ltl::default_environment& e =
     spot::ltl::default_environment::instance();
-  spot::taa_tgba_string* a = new spot::taa_tgba_string(dict);
+  spot::taa_tgba_string* a = new spot::taa_tgba_string(spot::make_bdd_dict());
 
   typedef spot::taa_tgba::transition trans;
 
@@ -49,7 +48,6 @@ main()
   spot::dotty_reachable(std::cout, a);
 
   delete a;
-  delete dict;
   assert(spot::ltl::atomic_prop::instance_count() == 0);
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
diff --git a/src/tgbatest/tgbaread.cc b/src/tgbatest/tgbaread.cc
index 6706d0a7d..5c7c8e782 100644
--- a/src/tgbatest/tgbaread.cc
+++ b/src/tgbatest/tgbaread.cc
@@ -52,7 +52,7 @@ main(int argc, char** argv)
       filename_index = 2;
     }
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::tgba_parse_error_list pel;
@@ -72,11 +72,9 @@ main(int argc, char** argv)
       return 1;
     }
 
-  delete dict;
   assert(spot::ltl::atomic_prop::instance_count() == 0);
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
   assert(spot::ltl::multop::instance_count() == 0);
-
   return 0;
 }
diff --git a/src/tgbatest/tripprod.cc b/src/tgbatest/tripprod.cc
index a712078f2..021c7f6a4 100644
--- a/src/tgbatest/tripprod.cc
+++ b/src/tgbatest/tripprod.cc
@@ -43,7 +43,7 @@ main(int argc, char** argv)
   if (argc != 4)
     syntax(argv[0]);
 
-  spot::bdd_dict* dict = new spot::bdd_dict();
+  auto dict = spot::make_bdd_dict();
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::tgba_parse_error_list pel1;
@@ -73,6 +73,5 @@ main(int argc, char** argv)
   delete a2;
   delete a3;
   assert(spot::ltl::atomic_prop::instance_count() == 0);
-  delete dict;
   return exit_code;
 }
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 4c784c0d3..fc47be371 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -493,7 +493,7 @@ cannot be translated using this algorithm.  Please use Couveur/FM.'''
                % format_formula(f, 'span'))
     finish()
 
-dict = spot.bdd_dict()
+dict = spot.make_bdd_dict()
 
 if output_type == 't' and not (f.is_ltl_formula() and f.is_X_free()):
     unbufprint('<b>Warning:</b> The following result assumes the input formula is stuttering insensitive.</br>')
diff --git a/wrap/python/tests/alarm.py b/wrap/python/tests/alarm.py
index 49e018c14..ee8cc85ea 100755
--- a/wrap/python/tests/alarm.py
+++ b/wrap/python/tests/alarm.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2012  Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2014  Laboratoire de Recherche et Développement
 # de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -45,7 +45,7 @@ P_Rbt2.moins || P_Rbt2.stop))-> G((F "map[0]==1") && (F "map[1]==1")
 e = spot.default_environment.instance()
 p = spot.empty_parse_error_list()
 f = spot.parse(f, p, e)
-d = spot.bdd_dict()
+d = spot.make_bdd_dict()
 
 spot.unblock_signal(signal.SIGALRM)
 spot.unblock_signal(signal.SIGTERM)
diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py
index c7bf1d9dd..e6825bb25 100755
--- a/wrap/python/tests/ltl2tgba.py
+++ b/wrap/python/tests/ltl2tgba.py
@@ -84,7 +84,7 @@ f = spot.parse(args[0], p, e, debug_opt)
 if spot.format_parse_errors(cerr, args[0], p):
     exit_code = 1
 
-dict = spot.bdd_dict()
+dict = spot.make_bdd_dict()
 
 if f:
     if fm_opt:
@@ -119,8 +119,6 @@ if f:
 else:
     exit_code = 1
 
-del dict;
-
 assert spot.atomic_prop.instance_count() == 0
 assert spot.unop.instance_count() == 0
 assert spot.binop.instance_count() == 0
diff --git a/wrap/python/tests/parsetgba.py b/wrap/python/tests/parsetgba.py
index 05abe5bb5..c593f9fd4 100755
--- a/wrap/python/tests/parsetgba.py
+++ b/wrap/python/tests/parsetgba.py
@@ -33,9 +33,8 @@ out = open(filename, 'w+')
 out.write(contents)
 out.close()
 
-d = spot.bdd_dict()
 p = spot.empty_tgba_parse_error_list()
-a = spot.tgba_parse(filename, p, d)
+a = spot.tgba_parse(filename, p, spot.make_bdd_dict())
 
 assert not p
 
@@ -43,6 +42,5 @@ spot.dotty_reachable(spot.get_cout(), a)
 
 del p
 del a
-del d
 
 os.unlink(filename)