diff --git a/spot/tl/derive.cc b/spot/tl/derive.cc
index 2b1873ed2..c6c328786 100644
--- a/spot/tl/derive.cc
+++ b/spot/tl/derive.cc
@@ -203,9 +203,9 @@ namespace spot
   }
 
   twa_graph_ptr
-  derive_finite_automaton_with_first(formula f, bool deterministic)
+  derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                                     bool deterministic)
   {
-    auto bdd_dict = make_bdd_dict();
     auto aut = make_twa_graph(bdd_dict);
 
     aut->prop_state_acc(true);
@@ -403,9 +403,11 @@ namespace spot
   }
 
   twa_graph_ptr
-  derive_automaton_with_first(formula f, bool deterministic)
+  derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                              bool deterministic)
   {
-    auto finite = derive_finite_automaton_with_first(f, deterministic);
+    auto finite = derive_finite_automaton_with_first(f, bdd_dict,
+                                                     deterministic);
 
     return from_finite(finite);
   }
diff --git a/spot/tl/derive.hh b/spot/tl/derive.hh
index 1947951ed..9e094c7b6 100644
--- a/spot/tl/derive.hh
+++ b/spot/tl/derive.hh
@@ -39,13 +39,15 @@ namespace spot
   derive_automaton(formula f, bool deterministic = true);
 
   SPOT_API twa_graph_ptr
-  derive_automaton_with_first(formula f, bool deterministic = true);
+  derive_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                              bool deterministic = true);
 
   SPOT_API twa_graph_ptr
   derive_finite_automaton(formula f, bool deterministic = true);
 
   SPOT_API twa_graph_ptr
-  derive_finite_automaton_with_first(formula f, bool deterministic = true);
+  derive_finite_automaton_with_first(formula f, bdd_dict_ptr bdd_dict,
+                                     bool deterministic = true);
 
   SPOT_API formula
   rewrite_and_nlm(formula f);
diff --git a/spot/twaalgos/translate_aa.cc b/spot/twaalgos/translate_aa.cc
index b15dfc279..0a29a0671 100644
--- a/spot/twaalgos/translate_aa.cc
+++ b/spot/twaalgos/translate_aa.cc
@@ -39,6 +39,11 @@ namespace spot
       {
       }
 
+      ~ltl_to_aa_builder()
+      {
+        aut_->get_dict()->unregister_all_my_variables(this);
+      }
+
       twa_graph_ptr aut_;
       unsigned accepting_sink_;
       internal::univ_dest_mapper<twa_graph::graph_t> uniq_;
@@ -241,9 +246,9 @@ namespace spot
           {
             // FIXME: combine out edges with rhs !
             //unsigned rhs_init = recurse(f[1]);
-            twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0]);
+            const auto& dict = aut_->get_dict();
+            twa_graph_ptr sere_aut = derive_finite_automaton_with_first(f[0], dict);
 
-            const auto& dict = sere_aut->get_dict();
 
             std::map<unsigned, unsigned> old_to_new;
             std::map<unsigned, int> state_to_var;
@@ -271,6 +276,7 @@ namespace spot
               return p.first->second;
             };
 
+            aut_->copy_ap_of(sere_aut);
             unsigned ns = sere_aut->num_states();
             for (unsigned st = 0; st < ns; ++st)
               {