diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc
index f88266ce6..8b0d0ba34 100644
--- a/spot/twaalgos/determinize.cc
+++ b/spot/twaalgos/determinize.cc
@@ -66,7 +66,7 @@ namespace spot
     compute_succs(const const_twa_graph_ptr& aut,
                   succs_t& res,
                   const scc_info& scc,
-                  const std::map<int, bdd>& implications,
+                  const std::vector<bdd>& implications,
                   const std::vector<bool>& is_connected,
                   std::unordered_map<bdd, unsigned, bdd_hash>& bdd2num,
                   std::vector<bdd>& all_bdds,
@@ -78,14 +78,14 @@ namespace spot
     compute_succ(const const_twa_graph_ptr& aut,
                  const bdd& ap,
                  const scc_info& scc,
-                 const std::map<int, bdd>& implications,
+                 const std::vector<bdd>& implications,
                  const std::vector<bool>& is_connected,
                  bool use_scc,
                  bool use_simulation) const;
     // The outermost brace of each node cannot be green
     void ungreenify_last_brace();
     // When a nodes a implies a node b, remove the node a.
-    void merge_redundant_states(const std::map<int, bdd>& implications,
+    void merge_redundant_states(const std::vector<bdd>& implications,
                                 const scc_info& scc,
                                 const std::vector<bool>& is_connected);
     // Used when creating the list of successors
@@ -252,7 +252,7 @@ namespace spot
   safra_state::compute_succ(const const_twa_graph_ptr& aut,
                             const bdd& ap,
                             const scc_info& scc,
-                            const std::map<int, bdd>& implications,
+                            const std::vector<bdd>& implications,
                             const std::vector<bool>& is_connected,
                             bool use_scc,
                             bool use_simulation) const
@@ -289,7 +289,7 @@ namespace spot
   safra_state::compute_succs(const const_twa_graph_ptr& aut,
                              succs_t& res,
                              const scc_info& scc,
-                             const std::map<int, bdd>& implications,
+                             const std::vector<bdd>& implications,
                              const std::vector<bool>& is_connected,
                              std::unordered_map<bdd, unsigned, bdd_hash>&
                              bdd2num,
@@ -337,7 +337,7 @@ namespace spot
   }
 
   void
-  safra_state::merge_redundant_states(const std::map<int, bdd>& implications,
+  safra_state::merge_redundant_states(const std::vector<bdd>& implications,
                                       const scc_info& scc,
                                       const std::vector<bool>& is_connected)
   {
@@ -590,7 +590,7 @@ namespace spot
 
     // Degeneralize
     twa_graph_ptr aut = spot::degeneralize_tba(a);
-    std::map<int, bdd> implications;
+    std::vector<bdd> implications;
     if (use_simulation)
       {
         aut = spot::scc_filter(aut);
diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index 8cb1c6e35..71ee82b4a 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -343,7 +343,7 @@ namespace spot
       }
 
       // The core loop of the algorithm.
-      twa_graph_ptr run(std::map<int, bdd>* implications = nullptr)
+      twa_graph_ptr run(std::vector<bdd>* implications = nullptr)
       {
         main_loop();
         return build_result(implications);
@@ -462,7 +462,7 @@ namespace spot
       }
 
       // Build the minimal resulting automaton.
-      twa_graph_ptr build_result(std::map<int, bdd>* implications = nullptr)
+      twa_graph_ptr build_result(std::vector<bdd>* implications = nullptr)
       {
         twa_graph_ptr res = make_twa_graph(a_->get_dict());
         res->copy_ap_of(a_);
@@ -473,6 +473,8 @@ namespace spot
 
         auto* gb = res->create_namer<int>();
 
+        if (implications)
+          implications->resize(bdd_lstate_.size());
         // Create one state per partition.
         for (auto& p: bdd_lstate_)
           {
@@ -711,7 +713,7 @@ namespace spot
 
   twa_graph_ptr
   simulation(const const_twa_graph_ptr& t,
-             std::map<int, bdd>* implications)
+             std::vector<bdd>* implications)
   {
     direct_simulation<false, false> simul(t);
     return simul.run(implications);
diff --git a/spot/twaalgos/simulation.hh b/spot/twaalgos/simulation.hh
index 3510b9e3f..07defa2e7 100644
--- a/spot/twaalgos/simulation.hh
+++ b/spot/twaalgos/simulation.hh
@@ -71,7 +71,7 @@ namespace spot
   simulation(const const_twa_graph_ptr& automaton);
   SPOT_API twa_graph_ptr
   simulation(const const_twa_graph_ptr& automaton,
-                      std::map<int, bdd>* implementation);
+             std::vector<bdd>* implications);
   SPOT_API twa_graph_ptr
   simulation_sba(const const_twa_graph_ptr& automaton);
   /// @}