diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc
index e92a74621..4a6e6ca0c 100644
--- a/spot/tl/expansions.cc
+++ b/spot/tl/expansions.cc
@@ -29,436 +29,6 @@ namespace spot
 {
   namespace
   {
-    class expansion_builder
-    {
-    public:
-      using exp_map = std::map<bdd, formula, bdd_less_than>;
-
-      virtual void insert(bdd letter, formula suffix) = 0;
-      virtual void finalize(bool deterministic) = 0;
-      virtual exp_map& result() = 0;
-      virtual bool empty() = 0;
-      virtual void clear() = 0;
-    };
-
-    class expansion_basic final : expansion_builder
-    {
-    public:
-      using exp_map = expansion_builder::exp_map;
-
-      expansion_basic(bdd_dict_ptr d)
-      {}
-
-      expansion_basic(exp_map&& m, bdd_dict_ptr d)
-        : bdd2formula_(m)
-        , formula2bdd_()
-      {}
-
-      void insert(bdd letter, formula suffix) final;
-
-      void finalize(bool deterministic) final;
-
-      exp_map& result() final
-      {
-        return bdd2formula_;
-      }
-
-      bool empty() final
-      {
-        return bdd2formula_.empty();
-      }
-
-      void clear() final
-      {
-        bdd2formula_.clear();
-      }
-
-    private:
-      exp_map bdd2formula_;
-      std::map<formula, exp_map::iterator> formula2bdd_;
-    };
-
-    void expansion_basic::insert(bdd letter, formula suffix)
-    {
-      auto res = bdd2formula_.insert({letter, suffix});
-      if (!res.second)
-        {
-          auto it = res.first;
-          it->second = formula::OrRat({it->second, suffix});
-        }
-    }
-
-    void expansion_basic::finalize(bool deterministic)
-    {
-      if (!deterministic)
-        return;
-
-      bdd or_labels = bddfalse;
-      bdd support = bddtrue;
-      bool is_det = true;
-      for (const auto& [l, _] : bdd2formula_)
-        {
-          support &= bdd_support(l);
-          if (is_det)
-            is_det = !bdd_have_common_assignment(l, or_labels);
-          or_labels |= l;
-        }
-
-      if (is_det)
-        {
-          // we don't need to determinize the expansion, it's already
-          // deterministic
-          return;
-        }
-
-      exp_map res;
-      std::vector<formula> dests;
-      for (bdd l: minterms_of(or_labels, support))
-        {
-          for (const auto& [ndet_label, ndet_dest] : bdd2formula_)
-            {
-              if (bdd_implies(l, ndet_label))
-                dests.push_back(ndet_dest);
-            }
-          formula or_dests = formula::OrRat(dests);
-          res.insert({l, or_dests});
-          dests.clear();
-        }
-
-      bdd2formula_ = std::move(res);
-    }
-
-    class expansion_merge_formulas final : expansion_builder
-    {
-    public:
-      using exp_map = expansion_builder::exp_map;
-
-      expansion_merge_formulas(bdd_dict_ptr d)
-      {}
-
-      expansion_merge_formulas(exp_map&& m, bdd_dict_ptr d)
-        : res_()
-        , terms_(m.begin(), m.end())
-      {}
-
-      void insert(bdd letter, formula suffix) final;
-
-      void finalize(bool deterministic) final;
-
-      exp_map& result() final
-      {
-        return res_;
-      }
-
-      bool empty() final
-      {
-        return terms_.empty();
-      }
-
-      void clear() final
-      {
-        terms_.clear();
-        res_.clear();
-      }
-
-    private:
-      std::vector<std::pair<bdd, formula>> terms_;
-      exp_map res_;
-    };
-
-    void expansion_merge_formulas::insert(bdd letter, formula suffix)
-    {
-      terms_.push_back({letter, suffix});
-    }
-
-    void expansion_merge_formulas::finalize(bool deterministic)
-    {
-      res_.clear();
-
-      // Given such terms:
-      //
-      // - a . ϕ1
-      // - a . ϕ2
-      // - b . ϕ1
-      //
-      // Merge them by suffix:
-      //
-      // - (a ∨ b) . ϕ1
-      // - a . ϕ2
-      std::map<formula, bdd> suffix2letter;
-      for (const auto& [letter, suffix]: terms_)
-        {
-          auto res = suffix2letter.insert({suffix, letter});
-          if (!res.second)
-            {
-              auto it = res.first;
-              it->second |= letter;
-            }
-        }
-
-      // Given such terms:
-      //
-      // - a . ϕ1
-      // - a . ϕ2
-      //
-      // Merge them by letter:
-      //
-      // - a . (ϕ1 ∨ ϕ2)
-      for (const auto& [suffix, letter]: suffix2letter)
-        {
-          auto res = res_.insert({letter, suffix});
-          if (!res.second)
-            {
-              auto it = res.first;
-              it->second = formula::OrRat({it->second, suffix});
-            }
-        }
-
-      if (!deterministic)
-        return;
-
-      bdd or_labels = bddfalse;
-      bdd support = bddtrue;
-      bool is_det = true;
-      for (const auto& [l, _] : res_)
-        {
-          support &= bdd_support(l);
-          if (is_det)
-            is_det = !bdd_have_common_assignment(l, or_labels);
-          or_labels |= l;
-        }
-
-      if (is_det)
-        {
-          // we don't need to determinize the expansion, it's already
-          // deterministic
-          return;
-        }
-
-      exp_map res;
-      std::vector<formula> dests;
-      for (bdd l: minterms_of(or_labels, support))
-        {
-          for (const auto& [ndet_label, ndet_dest] : res_)
-            {
-              if (bdd_implies(l, ndet_label))
-                dests.push_back(ndet_dest);
-            }
-          formula or_dests = formula::OrRat(dests);
-          res.insert({l, or_dests});
-          dests.clear();
-        }
-
-      res_ = std::move(res);
-    }
-
-    class expansion_bdd final : expansion_builder
-    {
-    public:
-      using exp_map = expansion_builder::exp_map;
-
-      expansion_bdd(bdd_dict_ptr d)
-        : anon_set_(bddtrue)
-        , d_(d)
-      {}
-
-      expansion_bdd(exp_map&& m, bdd_dict_ptr d)
-        : anon_set_(bddtrue)
-        , d_(d)
-      {
-        for (const auto& [letter, suffix] : m)
-          {
-            insert(letter, suffix);
-          }
-      }
-
-      expansion_bdd(const expansion_bdd&) = delete;
-
-      expansion_bdd&
-      operator=(const expansion_bdd& other) = delete;
-
-      expansion_bdd&
-      operator=(const expansion_bdd&& other)
-      {
-        d_->unregister_all_my_variables(this);
-
-        anon_set_ = std::move(other.anon_set_);
-        exp_ = std::move(other.exp_);
-        res_ = std::move(other.res_);
-        formula2bdd_ = std::move(other.formula2bdd_);
-        bdd2formula_ = std::move(other.bdd2formula_);
-
-        d_ = other.d_;
-        d_->register_all_variables_of(&other, this);
-
-        return *this;
-      }
-
-      ~expansion_bdd()
-      {
-        d_->unregister_all_my_variables(this);
-      }
-
-      void insert(bdd letter, formula suffix) final;
-
-      void finalize(bool deterministic) final;
-
-      exp_map& result() final
-      {
-        return res_;
-      }
-
-      bool empty() final
-      {
-        return formula2bdd_.empty();
-      }
-
-      void clear() final
-      {
-        formula2bdd_.clear();
-        bdd2formula_.clear();
-        exp_ = bddfalse;
-        anon_set_ = bddtrue;
-        res_.clear();
-      }
-
-    private:
-        bdd exp_;
-        bdd anon_set_;
-        std::map<formula, int> formula2bdd_;
-        std::map<int, formula> bdd2formula_;
-        exp_map res_;
-        bdd_dict_ptr d_;
-
-        formula var_to_formula(int var);
-        formula conj_bdd_to_sere(bdd b);
-        formula bdd_to_sere(bdd b);
-    };
-
-    formula
-    expansion_bdd::var_to_formula(int var)
-    {
-      formula f = bdd2formula_[var];
-      assert(f);
-      return f;
-    }
-
-    formula
-    expansion_bdd::conj_bdd_to_sere(bdd b)
-    {
-      if (b == bddtrue)
-        return formula::tt();
-      if (b == bddfalse)
-        return formula::ff();
-
-      // Unroll the first loop of the next do/while loop so that we
-      // do not have to create v when b is not a conjunction.
-      formula res = var_to_formula(bdd_var(b));
-      bdd high = bdd_high(b);
-      if (high == bddfalse)
-        {
-          res = formula::Not(res);
-          b = bdd_low(b);
-        }
-      else
-        {
-          assert(bdd_low(b) == bddfalse);
-          b = high;
-        }
-      if (b == bddtrue)
-        return res;
-      std::vector<formula> v{std::move(res)};
-      do
-        {
-          res = var_to_formula(bdd_var(b));
-          high = bdd_high(b);
-          if (high == bddfalse)
-            {
-              res = formula::Not(res);
-              b = bdd_low(b);
-            }
-          else
-            {
-              assert(bdd_low(b) == bddfalse);
-              b = high;
-            }
-          assert(b != bddfalse);
-          v.emplace_back(std::move(res));
-        }
-      while (b != bddtrue);
-      return formula::multop(op::AndRat, std::move(v));
-    }
-
-    void expansion_bdd::insert(bdd letter, formula suffix)
-    {
-
-      int anon_var_num;
-      auto it = formula2bdd_.find(suffix);
-      if (it != formula2bdd_.end())
-        {
-          anon_var_num = it->second;
-        }
-      else
-        {
-          anon_var_num = d_->register_anonymous_variables(1, this);
-          formula2bdd_.insert({suffix, anon_var_num});
-          bdd2formula_.insert({anon_var_num, suffix});
-        }
-
-      bdd var = bdd_ithvar(anon_var_num);
-      anon_set_ &= var;
-      exp_ |= letter & var;
-    }
-      formula
-      expansion_bdd::bdd_to_sere(bdd f)
-      {
-        if (f == bddfalse)
-          return formula::ff();
-
-        std::vector<formula> v;
-        minato_isop isop(f);
-        bdd cube;
-        while ((cube = isop.next()) != bddfalse)
-          v.emplace_back(conj_bdd_to_sere(cube));
-        return formula::OrRat(std::move(v));
-      }
-
-    void expansion_bdd::finalize(bool deterministic)
-    {
-      if (deterministic)
-        {
-          bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
-          bdd or_labels = bdd_exist(exp_, anon_set_);
-          for (bdd letter: minterms_of(exp_, prop_set))
-            {
-              bdd dest_bdd = bdd_restrict(exp_, letter);
-              formula dest = bdd_to_sere(dest_bdd);
-
-              auto it = res_.insert({letter, dest});
-              assert(it.second);
-              (void) it;
-            }
-        }
-      else
-        {
-          minato_isop isop(exp_);
-          bdd cube;
-          while ((cube = isop.next()) != bddfalse)
-            {
-              bdd letter = bdd_exist(cube, anon_set_);
-              bdd suffix = bdd_existcomp(cube, anon_set_);
-              formula dest = conj_bdd_to_sere(suffix);
-
-              auto it = res_.insert({letter, dest});
-              if (!it.second)
-                {
-                  auto it2 = it.first;
-                  it2->second = formula::OrRat({it2->second, dest});
-                }
-            }
-        }
-    }
-
     // FIXME: could probably just return a map directly
     static std::vector<std::string>
     formula_aps(formula f)
@@ -479,8 +49,8 @@ namespace spot
       return std::vector(res.begin(), res.end());
     }
 
-  formula
-  rewrite_and_nlm(formula f)
+    formula
+    rewrite_and_nlm(formula f)
     {
       unsigned s = f.size();
       std::vector<formula> final;
@@ -532,30 +102,15 @@ namespace spot
       }
       return formula::OrRat(std::move(disj));
     }
-  }
 
-  formula
-  expansion_to_formula(expansion_t e, bdd_dict_ptr& d)
-  {
-    std::vector<formula> res;
-
-    for (const auto& [key, val] : e)
-      {
-        formula prefix = bdd_to_formula(key, d);
-        res.push_back(formula::Concat({prefix, val}));
-      }
-
-    return formula::OrRat(res);
-  }
-
-  class bdd_finalizer
-  {
-    public:
-      bdd_finalizer(std::multimap<bdd, formula, bdd_less_than>& exp, bdd_dict_ptr d)
-        : anon_set_(bddtrue)
-        , d_(d)
-      {
-        for (const auto& [prefix, suffix] : exp)
+    class bdd_finalizer
+    {
+      public:
+        bdd_finalizer(std::multimap<bdd, formula, bdd_less_than>& exp, bdd_dict_ptr d)
+          : anon_set_(bddtrue)
+          , d_(d)
+        {
+          for (const auto& [prefix, suffix] : exp)
           {
             int anon_var_num;
             auto it = formula2bdd_.find(suffix);
@@ -574,185 +129,201 @@ namespace spot
             anon_set_ &= var;
             exp_ |= prefix & var;
           }
-      }
+        }
 
-      ~bdd_finalizer()
-      {
-        d_->unregister_all_my_variables(this);
-      }
+        ~bdd_finalizer()
+        {
+          d_->unregister_all_my_variables(this);
+        }
 
-      std::multimap<bdd, formula, bdd_less_than>
-      simplify(exp_opts_new::expand_opt_new opts);
+        expansion_t
+        simplify(exp_opts::expand_opt opts);
 
-    private:
-      bdd exp_;
-      bdd anon_set_;
-      std::map<formula, int> formula2bdd_;
-      std::map<int, formula> bdd2formula_;
-      bdd_dict_ptr d_;
+      private:
+        bdd exp_;
+        bdd anon_set_;
+        std::map<formula, int> formula2bdd_;
+        std::map<int, formula> bdd2formula_;
+        bdd_dict_ptr d_;
 
-      formula var_to_formula(int var);
-      formula conj_bdd_to_sere(bdd b);
-      formula bdd_to_sere(bdd b);
-  };
+        formula var_to_formula(int var);
+        formula conj_bdd_to_sere(bdd b);
+        formula bdd_to_sere(bdd b);
+    };
 
-  formula
-  bdd_finalizer::var_to_formula(int var)
-  {
-    formula f = bdd2formula_[var];
-    assert(f);
-    return f;
-  }
+    formula
+    bdd_finalizer::var_to_formula(int var)
+    {
+      formula f = bdd2formula_[var];
+      assert(f);
+      return f;
+    }
 
-  formula
-  bdd_finalizer::bdd_to_sere(bdd f)
-  {
-    if (f == bddfalse)
-      return formula::ff();
+    formula
+    bdd_finalizer::bdd_to_sere(bdd f)
+    {
+      if (f == bddfalse)
+        return formula::ff();
 
-    std::vector<formula> v;
-    minato_isop isop(f);
-    bdd cube;
-    while ((cube = isop.next()) != bddfalse)
-      v.emplace_back(conj_bdd_to_sere(cube));
-    return formula::OrRat(std::move(v));
-  }
+      std::vector<formula> v;
+      minato_isop isop(f);
+      bdd cube;
+      while ((cube = isop.next()) != bddfalse)
+        v.emplace_back(conj_bdd_to_sere(cube));
+      return formula::OrRat(std::move(v));
+    }
 
-  formula
-  bdd_finalizer::conj_bdd_to_sere(bdd b)
-  {
-    if (b == bddtrue)
-      return formula::tt();
-    if (b == bddfalse)
-      return formula::ff();
+    formula
+    bdd_finalizer::conj_bdd_to_sere(bdd b)
+    {
+      if (b == bddtrue)
+        return formula::tt();
+      if (b == bddfalse)
+        return formula::ff();
 
-    // Unroll the first loop of the next do/while loop so that we
-    // do not have to create v when b is not a conjunction.
-    formula res = var_to_formula(bdd_var(b));
-    bdd high = bdd_high(b);
-    if (high == bddfalse)
+      // Unroll the first loop of the next do/while loop so that we
+      // do not have to create v when b is not a conjunction.
+      formula res = var_to_formula(bdd_var(b));
+      bdd high = bdd_high(b);
+      if (high == bddfalse)
       {
         res = formula::Not(res);
         b = bdd_low(b);
       }
-    else
+      else
       {
         assert(bdd_low(b) == bddfalse);
         b = high;
       }
-    if (b == bddtrue)
-      return res;
-    std::vector<formula> v{std::move(res)};
-    do
+      if (b == bddtrue)
+        return res;
+      std::vector<formula> v{std::move(res)};
+      do
       {
         res = var_to_formula(bdd_var(b));
         high = bdd_high(b);
         if (high == bddfalse)
-          {
-            res = formula::Not(res);
-            b = bdd_low(b);
-          }
+        {
+          res = formula::Not(res);
+          b = bdd_low(b);
+        }
         else
-          {
-            assert(bdd_low(b) == bddfalse);
-            b = high;
-          }
+        {
+          assert(bdd_low(b) == bddfalse);
+          b = high;
+        }
         assert(b != bddfalse);
         v.emplace_back(std::move(res));
       }
-    while (b != bddtrue);
-    return formula::multop(op::AndRat, std::move(v));
-  }
-
-  std::multimap<bdd, formula, bdd_less_than>
-  bdd_finalizer::simplify(exp_opts_new::expand_opt_new opts)
-  {
-    std::multimap<bdd, formula, bdd_less_than> res;
-
-    if (opts & exp_opts_new::expand_opt_new::BddMinterm)
-    {
-      bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
-      bdd or_labels = bdd_exist(exp_, anon_set_);
-      for (bdd letter: minterms_of(exp_, prop_set))
-      {
-        bdd dest_bdd = bdd_restrict(exp_, letter);
-        formula dest = bdd_to_sere(dest_bdd);
-
-        auto it = res.insert({letter, dest});
-        assert(it.second);
-        (void) it;
-      }
-    }
-    else // BddIsop
-    {
-      minato_isop isop(exp_);
-      bdd cube;
-      while ((cube = isop.next()) != bddfalse)
-      {
-        bdd letter = bdd_exist(cube, anon_set_);
-        bdd suffix = bdd_existcomp(cube, anon_set_);
-        formula dest = conj_bdd_to_sere(suffix);
-
-        res.insert({letter, dest});
-      }
+      while (b != bddtrue);
+      return formula::multop(op::AndRat, std::move(v));
     }
 
-    return res;
-  }
+    expansion_t
+    bdd_finalizer::simplify(exp_opts::expand_opt opts)
+    {
+      expansion_t res;
 
-  void
-  finalize_new(std::multimap<bdd, formula, bdd_less_than>& exp, exp_opts_new::expand_opt_new opts, bdd_dict_ptr d)
-  {
-    if (opts & (exp_opts_new::expand_opt_new::BddIsop
-                | exp_opts_new::expand_opt_new::BddMinterm))
+      if (opts & exp_opts::expand_opt::BddMinterm)
+      {
+        bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
+        bdd or_labels = bdd_exist(exp_, anon_set_);
+        for (bdd letter: minterms_of(exp_, prop_set))
+        {
+          bdd dest_bdd = bdd_restrict(exp_, letter);
+          formula dest = bdd_to_sere(dest_bdd);
+
+          auto it = res.insert({letter, dest});
+          assert(it.second);
+          (void) it;
+        }
+      }
+      else // BddIsop
+      {
+        minato_isop isop(exp_);
+        bdd cube;
+        while ((cube = isop.next()) != bddfalse)
+        {
+          bdd letter = bdd_exist(cube, anon_set_);
+          bdd suffix = bdd_existcomp(cube, anon_set_);
+          formula dest = conj_bdd_to_sere(suffix);
+
+          res.insert({letter, dest});
+        }
+      }
+
+      return res;
+    }
+
+    void
+    finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d)
+    {
+      if (opts & (exp_opts::expand_opt::BddIsop
+                  | exp_opts::expand_opt::BddMinterm))
       {
         bdd_finalizer bddf(exp, d);
         exp = bddf.simplify(opts);
       }
 
-    if (opts & exp_opts_new::expand_opt_new::UniqueSuffix)
+      if (opts & exp_opts::expand_opt::UniqueSuffix)
       {
         std::map<formula, bdd> unique_map;
         for (const auto& [prefix, suffix] : exp)
+        {
+          auto res = unique_map.insert({suffix, prefix});
+          if (!res.second)
           {
-            auto res = unique_map.insert({suffix, prefix});
-            if (!res.second)
-              {
-                auto it = res.first;
-                it->second |= prefix;
-              }
+            auto it = res.first;
+            it->second |= prefix;
           }
+        }
 
         exp.clear();
         for (const auto [suffix, prefix] : unique_map)
-          {
-            exp.insert({prefix, suffix});
-          }
+        {
+          exp.insert({prefix, suffix});
+        }
       }
 
-    if (opts & exp_opts_new::expand_opt_new::UniquePrefix)
+      if (opts & exp_opts::expand_opt::UniquePrefix)
       {
         std::map<bdd, formula, bdd_less_than> unique_map;
         for (const auto& [prefix, suffix] : exp)
+        {
+          auto res = unique_map.insert({prefix, suffix});
+          if (!res.second)
           {
-            auto res = unique_map.insert({prefix, suffix});
-            if (!res.second)
-            {
-              auto it = res.first;
-              it->second = formula::OrRat({it->second, suffix});
-            }
+            auto it = res.first;
+            it->second = formula::OrRat({it->second, suffix});
           }
+        }
 
         exp.clear();
         for (const auto [prefix, suffix] : unique_map)
-          {
-            exp.insert({prefix, suffix});
-          }
+        {
+          exp.insert({prefix, suffix});
+        }
       }
+    }
   }
 
-  std::multimap<bdd, formula, bdd_less_than>
-  expansion_new(formula f, const bdd_dict_ptr& d, void *owner, exp_opts_new::expand_opt_new opts)
+  formula
+  expansion_to_formula(expansion_t e, bdd_dict_ptr& d)
+  {
+    std::vector<formula> res;
+
+    for (const auto& [key, val] : e)
+      {
+        formula prefix = bdd_to_formula(key, d);
+        res.push_back(formula::Concat({prefix, val}));
+      }
+
+    return formula::OrRat(res);
+  }
+
+
+  expansion_t
+  expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts)
   {
     using exp_t = std::multimap<bdd, formula, bdd_less_than>;
 
@@ -767,7 +338,7 @@ namespace spot
       }
 
     auto rec = [&d, owner, opts](formula f){
-      return expansion_new(f, d, owner, exp_opts_new::None);
+      return expansion(f, d, owner, exp_opts::None);
     };
 
 
@@ -800,7 +371,7 @@ namespace spot
                   }
               }
 
-            finalize_new(res, opts, d);
+            finalize(res, opts, d);
             return res;
           }
 
@@ -837,7 +408,7 @@ namespace spot
             if (f.min() == 0)
               res.insert({bddtrue, formula::eword()});
 
-            finalize_new(res, opts, d);
+            finalize(res, opts, d);
             return res;
           }
 
@@ -856,7 +427,7 @@ namespace spot
                 res.insert({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
               }
 
-            finalize_new(res, opts, d);
+            finalize(res, opts, d);
             return res;
           }
 
@@ -864,7 +435,7 @@ namespace spot
           {
             formula rewrite = rewrite_and_nlm(f);
             auto res = rec(rewrite);
-            finalize_new(res, opts, d);
+            finalize(res, opts, d);
             return res;
           }
 
@@ -894,7 +465,7 @@ namespace spot
               {
                 for (auto& [_, dest] : res)
                   dest = formula::first_match(dest);
-                finalize_new(res, opts, d);
+                finalize(res, opts, d);
                 return res;
               }
 
@@ -914,7 +485,7 @@ namespace spot
 
             for (auto& [_, dest] : res_det)
               dest = formula::first_match(dest);
-            finalize_new(res_det, opts, d);
+            finalize(res_det, opts, d);
             return res_det;
           }
 
@@ -939,7 +510,7 @@ namespace spot
                 res.insert({li, formula::Fusion({ei, F})});
               }
 
-            finalize_new(res, opts, d);
+            finalize(res, opts, d);
             return res;
           }
 
@@ -978,7 +549,7 @@ namespace spot
                 res = std::move(new_res);
               }
 
-            finalize_new(res, opts, d);
+            finalize(res, opts, d);
             return res;
           }
 
@@ -1001,7 +572,7 @@ namespace spot
                   res.insert({label, dest});
               }
 
-            finalize_new(res, opts, d);
+            finalize(res, opts, d);
             return res;
           }
 
@@ -1015,498 +586,6 @@ namespace spot
     return {};
   }
 
-  std::multimap<bdd, formula, bdd_less_than>
-  expansion_simple(formula f, const bdd_dict_ptr& d, void *owner)
-  {
-    using exp_t = std::multimap<bdd, formula, bdd_less_than>;
-
-    if (f.is_boolean())
-      {
-        auto f_bdd = formula_to_bdd(f, d, owner);
-
-        if (f_bdd == bddfalse)
-          return {};
-
-        return {{f_bdd, formula::eword()}};
-      }
-
-    auto rec = [&d, owner](formula f){
-      return expansion_simple(f, d, owner);
-    };
-
-
-    switch (f.kind())
-      {
-        case op::ff:
-        case op::tt:
-        case op::ap:
-          SPOT_UNREACHABLE();
-
-        case op::eword:
-          return {{bddfalse, formula::ff()}};
-
-        case op::Concat:
-          {
-            auto exps = rec(f[0]);
-
-            exp_t res;
-            for (const auto& [bdd_l, form] : exps)
-              {
-                res.insert({bdd_l, formula::Concat({form, f.all_but(0)})});
-              }
-
-            if (f[0].accepts_eword())
-              {
-                auto exps_rest = rec(f.all_but(0));
-                for (const auto& [bdd_l, form] : exps_rest)
-                  {
-                    res.insert({bdd_l, form});
-                  }
-              }
-
-            return res;
-          }
-
-        case op::FStar:
-          {
-            formula E = f[0];
-
-            if (f.min() == 0 && f.max() == 0)
-              return {{bddtrue, formula::eword()}};
-
-            auto min = f.min() == 0 ? 0 : (f.min() - 1);
-            auto max = f.max() == formula::unbounded()
-                         ? formula::unbounded()
-                         : (f.max() - 1);
-
-            auto E_i_j_minus = formula::FStar(E, min, max);
-
-            auto exp = rec(E);
-            exp_t res;
-            for (const auto& [li, ei] : exp)
-              {
-                res.insert({li, formula::Fusion({ei, E_i_j_minus})});
-
-                if (ei.accepts_eword() && f.min() != 0)
-                  {
-                    for (const auto& [ki, fi] : rec(E_i_j_minus))
-                      {
-                        // FIXME: build bdd once
-                        if ((li & ki) != bddfalse)
-                          res.insert({li & ki, fi});
-                      }
-                  }
-              }
-            if (f.min() == 0)
-              res.insert({bddtrue, formula::eword()});
-
-            return res;
-          }
-
-        case op::Star:
-          {
-            auto min = f.min() == 0 ? 0 : (f.min() - 1);
-            auto max = f.max() == formula::unbounded()
-                         ? formula::unbounded()
-                         : (f.max() - 1);
-
-            auto exps = rec(f[0]);
-
-            exp_t res;
-            for (const auto& [bdd_l, form] : exps)
-              {
-                res.insert({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
-              }
-
-            return res;
-          }
-
-        case op::AndNLM:
-          {
-            formula rewrite = rewrite_and_nlm(f);
-            return rec(rewrite);
-          }
-
-        case op::first_match:
-          {
-            auto exps = rec(f[0]);
-
-            exp_t res;
-            for (const auto& [bdd_l, form] : exps)
-              {
-                res.insert({bdd_l, form});
-              }
-
-            // determinize
-            bdd or_labels = bddfalse;
-            bdd support = bddtrue;
-            bool is_det = true;
-            for (const auto& [l, _] : res)
-              {
-                support &= bdd_support(l);
-                if (is_det)
-                  is_det = !bdd_have_common_assignment(l, or_labels);
-                or_labels |= l;
-              }
-
-            if (is_det)
-              return res;
-
-            exp_t res_det;
-            std::vector<formula> dests;
-            for (bdd l: minterms_of(or_labels, support))
-              {
-                for (const auto& [ndet_label, ndet_dest] : res)
-                  {
-                    if (bdd_implies(l, ndet_label))
-                      dests.push_back(ndet_dest);
-                  }
-                formula or_dests = formula::OrRat(dests);
-                res_det.insert({l, or_dests});
-                dests.clear();
-              }
-
-            for (auto& [_, dest] : res_det)
-              dest = formula::first_match(dest);
-            return res_det;
-          }
-
-        case op::Fusion:
-          {
-            exp_t res;
-            formula E = f[0];
-            formula F = f.all_but(0);
-
-            exp_t Ei = rec(E);
-            // TODO: std::option
-            exp_t Fj = rec(F);
-
-            for (const auto& [li, ei] : Ei)
-              {
-                if (ei.accepts_eword())
-                  {
-                    for (const auto& [kj, fj] : Fj)
-                        if ((li & kj) != bddfalse)
-                          res.insert({li & kj, fj});
-                  }
-                res.insert({li, formula::Fusion({ei, F})});
-              }
-
-            return res;
-          }
-
-        case op::AndRat:
-          {
-            exp_t res;
-            for (const auto& sub_f : f)
-              {
-                auto exps = rec(sub_f);
-
-                if (exps.empty())
-                  {
-                    // op::AndRat: one of the expansions was empty (the only
-                    //             edge was `false`), so the AndRat is empty as
-                    //             well
-                    res.clear();
-                    break;
-                  }
-
-                if (res.empty())
-                  {
-                    res = std::move(exps);
-                    continue;
-                  }
-
-                exp_t new_res;
-                for (const auto& [l_key, l_val] : exps)
-                  {
-                    for (const auto& [r_key, r_val] : res)
-                      {
-                        if ((l_key & r_key) != bddfalse)
-                          new_res.insert({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})});
-                      }
-                  }
-
-                res = std::move(new_res);
-              }
-
-            return res;
-          }
-
-        case op::OrRat:
-          {
-            exp_t res;
-            for (const auto& sub_f : f)
-              {
-                auto exps = rec(sub_f);
-                if (exps.empty())
-                  continue;
-
-                if (res.empty())
-                  {
-                    res = std::move(exps);
-                    continue;
-                  }
-
-                for (const auto& [label, dest] : exps)
-                  res.insert({label, dest});
-              }
-
-            return res;
-          }
-
-        default:
-          std::cerr << "unimplemented kind "
-                    << static_cast<int>(f.kind())
-                    << std::endl;
-          SPOT_UNIMPLEMENTED();
-      }
-
-    return {};
-  }
-
-  template<typename ExpansionBuilder>
-  expansion_t
-  expansion_impl(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts)
-  {
-    if (f.is_boolean())
-      {
-        auto f_bdd = formula_to_bdd(f, d, owner);
-
-        if (f_bdd == bddfalse)
-          return {};
-
-        return {{f_bdd, formula::eword()}};
-      }
-
-    auto rec = [&d, owner](formula f){
-      return expansion_impl<ExpansionBuilder>(f, d, owner, exp_opts::None);
-    };
-
-
-    switch (f.kind())
-      {
-        case op::ff:
-        case op::tt:
-        case op::ap:
-          SPOT_UNREACHABLE();
-
-        case op::eword:
-          return {{bddfalse, formula::ff()}};
-
-        case op::Concat:
-          {
-            auto exps = rec(f[0]);
-
-            ExpansionBuilder res(d);
-            for (const auto& [bdd_l, form] : exps)
-              {
-                res.insert(bdd_l, formula::Concat({form, f.all_but(0)}));
-              }
-
-            if (f[0].accepts_eword())
-              {
-                auto exps_rest = rec(f.all_but(0));
-                for (const auto& [bdd_l, form] : exps_rest)
-                  {
-                    res.insert(bdd_l, form);
-                  }
-              }
-
-            res.finalize(opts & exp_opts::Deterministic);
-            return res.result();
-          }
-
-        case op::FStar:
-          {
-            formula E = f[0];
-
-            if (f.min() == 0 && f.max() == 0)
-              return {{bddtrue, formula::eword()}};
-
-            auto min = f.min() == 0 ? 0 : (f.min() - 1);
-            auto max = f.max() == formula::unbounded()
-                         ? formula::unbounded()
-                         : (f.max() - 1);
-
-            auto E_i_j_minus = formula::FStar(E, min, max);
-
-            auto exp = rec(E);
-            ExpansionBuilder res(d);
-            for (const auto& [li, ei] : exp)
-              {
-                res.insert(li, formula::Fusion({ei, E_i_j_minus}));
-
-                if (ei.accepts_eword() && f.min() != 0)
-                  {
-                    for (const auto& [ki, fi] : rec(E_i_j_minus))
-                      {
-                        // FIXME: build bdd once
-                        if ((li & ki) != bddfalse)
-                          res.insert(li & ki, fi);
-                      }
-                  }
-              }
-            if (f.min() == 0)
-              res.insert(bddtrue, formula::eword());
-
-            res.finalize(opts & exp_opts::Deterministic);
-            return res.result();
-          }
-
-        case op::Star:
-          {
-            auto min = f.min() == 0 ? 0 : (f.min() - 1);
-            auto max = f.max() == formula::unbounded()
-                         ? formula::unbounded()
-                         : (f.max() - 1);
-
-            auto exps = rec(f[0]);
-
-            ExpansionBuilder res(d);
-            for (const auto& [bdd_l, form] : exps)
-              {
-                res.insert(bdd_l, formula::Concat({form, formula::Star(f[0], min, max)}));
-              }
-
-            res.finalize(opts & exp_opts::Deterministic);
-            return res.result();
-          }
-
-        case op::AndNLM:
-          {
-            formula rewrite = rewrite_and_nlm(f);
-            return rec(rewrite);
-          }
-
-        case op::first_match:
-          {
-            auto exps = rec(f[0]);
-
-            ExpansionBuilder res(d);
-            for (const auto& [bdd_l, form] : exps)
-              {
-                res.insert(bdd_l, form);
-              }
-
-            res.finalize(true);
-            auto res2 = res.result();
-            for (auto& [_, dest] : res2)
-              dest = formula::first_match(dest);
-            return res2;
-          }
-
-        case op::Fusion:
-          {
-            ExpansionBuilder res(d);
-            formula E = f[0];
-            formula F = f.all_but(0);
-
-            expansion_t Ei = rec(E);
-            // TODO: std::option
-            expansion_t Fj = rec(F);
-
-            for (const auto& [li, ei] : Ei)
-              {
-                if (ei.accepts_eword())
-                  {
-                    for (const auto& [kj, fj] : Fj)
-                        if ((li & kj) != bddfalse)
-                          res.insert(li & kj, fj);
-                  }
-                res.insert(li, formula::Fusion({ei, F}));
-              }
-
-            res.finalize(opts & exp_opts::Deterministic);
-            return res.result();
-          }
-
-        case op::AndRat:
-          {
-            ExpansionBuilder res(d);
-            for (const auto& sub_f : f)
-              {
-                auto exps = rec(sub_f);
-
-                if (exps.empty())
-                  {
-                    // op::AndRat: one of the expansions was empty (the only
-                    //             edge was `false`), so the AndRat is empty as
-                    //             well
-                    res.clear();
-                    break;
-                  }
-
-                if (res.empty())
-                  {
-                    res = ExpansionBuilder(std::move(exps), d);
-                    res.finalize(false);
-                    continue;
-                  }
-
-                ExpansionBuilder new_res(d);
-                for (const auto& [l_key, l_val] : exps)
-                  {
-                    for (const auto& [r_key, r_val] : res.result())
-                      {
-                        if ((l_key & r_key) != bddfalse)
-                          new_res.insert(l_key & r_key, formula::multop(f.kind(), {l_val, r_val}));
-                      }
-                  }
-
-                res = std::move(new_res);
-                res.finalize(false);
-              }
-
-            res.finalize(opts & exp_opts::Deterministic);
-            return res.result();
-          }
-
-        case op::OrRat:
-          {
-            ExpansionBuilder res(d);
-            for (const auto& sub_f : f)
-              {
-                auto exps = rec(sub_f);
-                if (exps.empty())
-                  continue;
-
-                if (res.empty())
-                  {
-                    res = ExpansionBuilder(std::move(exps), d);
-                    continue;
-                  }
-
-                for (const auto& [label, dest] : exps)
-                  res.insert(label, dest);
-              }
-
-            res.finalize(opts & exp_opts::Deterministic);
-            return res.result();
-          }
-
-        default:
-          std::cerr << "unimplemented kind "
-                    << static_cast<int>(f.kind())
-                    << std::endl;
-          SPOT_UNIMPLEMENTED();
-      }
-
-    return {};
-  }
-
-  expansion_t
-  expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts)
-  {
-
-    if (opts & exp_opts::Bdd)
-      return expansion_impl<expansion_bdd>(f, d, owner, opts);
-    else if (opts & exp_opts::MergeSuffix)
-      return expansion_impl<expansion_merge_formulas>(f, d, owner, opts);
-    else // exp_opts::Basic
-      return expansion_impl<expansion_basic>(f, d, owner, opts);
-  }
-
   twa_graph_ptr
   expand_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts)
   {
@@ -1589,181 +668,9 @@ namespace spot
       }
 
     aut->set_named_prop("state-names", state_names);
-    aut->merge_edges();
-    return aut;
-  }
 
-  twa_graph_ptr
-  expand_simple_automaton(formula f, bdd_dict_ptr d)
-  {
-    auto finite = expand_simple_finite_automaton(f, d);
-    return from_finite(finite);
-  }
-
-  twa_graph_ptr
-  expand_simple_finite_automaton(formula f, bdd_dict_ptr d)
-  {
-    auto aut = make_twa_graph(d);
-
-    aut->prop_state_acc(true);
-    const auto acc_mark = aut->set_buchi();
-
-    auto formula2state = robin_hood::unordered_map<formula, unsigned>();
-
-    unsigned init_state = aut->new_state();
-    aut->set_init_state(init_state);
-    formula2state.insert({ f, init_state });
-
-    auto f_aps = formula_aps(f);
-    for (auto& ap : f_aps)
-        aut->register_ap(ap);
-
-    auto todo = std::vector<std::pair<formula, unsigned>>();
-    todo.push_back({f, init_state});
-
-    auto state_names = new std::vector<std::string>();
-    std::ostringstream ss;
-    ss << f;
-    state_names->push_back(ss.str());
-
-    auto find_dst = [&](formula suffix) -> unsigned
-      {
-        unsigned dst;
-        auto it = formula2state.find(suffix);
-        if (it != formula2state.end())
-        {
-          dst = it->second;
-        }
-        else
-        {
-          dst = aut->new_state();
-          todo.push_back({suffix, dst});
-          formula2state.insert({suffix, dst});
-          std::ostringstream ss;
-          ss << suffix;
-          state_names->push_back(ss.str());
-        }
-
-        return dst;
-      };
-
-    while (!todo.empty())
-      {
-        auto [curr_f, curr_state] = todo[todo.size() - 1];
-        todo.pop_back();
-
-        auto curr_acc_mark= curr_f.accepts_eword()
-          ? acc_mark
-          : acc_cond::mark_t();
-
-        auto exp = expansion_simple(curr_f, d, aut.get());
-
-        for (const auto& [letter, suffix] : exp)
-          {
-            if (suffix.is(op::ff))
-              continue;
-
-            auto dst = find_dst(suffix);
-            aut->new_edge(curr_state, dst, letter, curr_acc_mark);
-          }
-
-        // if state has no transitions and should be accepting, create
-        // artificial transition
-        if (aut->get_graph().state_storage(curr_state).succ == 0
-            && curr_f.accepts_eword())
-          aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
-      }
-
-    aut->set_named_prop("state-names", state_names);
-    aut->merge_edges();
-    return aut;
-  }
-
-  twa_graph_ptr
-  expand_new_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts)
-  {
-    auto finite = expand_new_finite_automaton(f, d, opts);
-    return from_finite(finite);
-  }
-
-  twa_graph_ptr
-  expand_new_finite_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts)
-  {
-    auto aut = make_twa_graph(d);
-
-    aut->prop_state_acc(true);
-    const auto acc_mark = aut->set_buchi();
-
-    auto formula2state = robin_hood::unordered_map<formula, unsigned>();
-
-    unsigned init_state = aut->new_state();
-    aut->set_init_state(init_state);
-    formula2state.insert({ f, init_state });
-
-    auto f_aps = formula_aps(f);
-    for (auto& ap : f_aps)
-        aut->register_ap(ap);
-
-    auto todo = std::vector<std::pair<formula, unsigned>>();
-    todo.push_back({f, init_state});
-
-    auto state_names = new std::vector<std::string>();
-    std::ostringstream ss;
-    ss << f;
-    state_names->push_back(ss.str());
-
-    auto find_dst = [&](formula suffix) -> unsigned
-      {
-        unsigned dst;
-        auto it = formula2state.find(suffix);
-        if (it != formula2state.end())
-        {
-          dst = it->second;
-        }
-        else
-        {
-          dst = aut->new_state();
-          todo.push_back({suffix, dst});
-          formula2state.insert({suffix, dst});
-          std::ostringstream ss;
-          ss << suffix;
-          state_names->push_back(ss.str());
-        }
-
-        return dst;
-      };
-
-    while (!todo.empty())
-      {
-        auto [curr_f, curr_state] = todo[todo.size() - 1];
-        todo.pop_back();
-
-        auto curr_acc_mark= curr_f.accepts_eword()
-          ? acc_mark
-          : acc_cond::mark_t();
-
-        auto exp = expansion_new(curr_f, d, aut.get(), opts);
-
-        for (const auto& [letter, suffix] : exp)
-          {
-            if (suffix.is(op::ff))
-              continue;
-
-            auto dst = find_dst(suffix);
-            aut->new_edge(curr_state, dst, letter, curr_acc_mark);
-          }
-
-        // if state has no transitions and should be accepting, create
-        // artificial transition
-        if (aut->get_graph().state_storage(curr_state).succ == 0
-            && curr_f.accepts_eword())
-          aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
-      }
-
-    aut->set_named_prop("state-names", state_names);
-
-    if ((opts & exp_opts_new::MergeEdges)
-        && !(opts & exp_opts_new::UniqueSuffix))
+    if ((opts & exp_opts::MergeEdges)
+        && !(opts & exp_opts::UniqueSuffix))
       aut->merge_edges();
 
     return aut;
diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh
index 52e83917f..43a51e721 100644
--- a/spot/tl/expansions.hh
+++ b/spot/tl/expansions.hh
@@ -30,22 +30,11 @@
 
 namespace spot
 {
-  using expansion_t = std::map<bdd, formula, bdd_less_than>;
+  using expansion_t = std::multimap<bdd, formula, bdd_less_than>;
 
   struct exp_opts
   {
     enum expand_opt {
-      None = 0,
-      Deterministic = 1,
-      Basic = 2,
-      MergeSuffix = 4,
-      Bdd = 8,
-    };
-  };
-
-  struct exp_opts_new
-  {
-    enum expand_opt_new {
       None = 0,
       UniqueSuffix = 1,
       UniquePrefix = 2,
@@ -55,33 +44,15 @@ namespace spot
     };
   };
 
-  SPOT_API std::multimap<bdd, formula, bdd_less_than>
-  expansion_new(formula f, const bdd_dict_ptr& d, void *owner, exp_opts_new::expand_opt_new opts);
-
-  SPOT_API twa_graph_ptr
-  expand_new_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts);
-
-  SPOT_API twa_graph_ptr
-  expand_new_finite_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts);
-
-  SPOT_API twa_graph_ptr
-  expand_simple_automaton(formula f, bdd_dict_ptr d);
-
-  SPOT_API twa_graph_ptr
-  expand_simple_finite_automaton(formula f, bdd_dict_ptr d);
-
-  SPOT_API std::multimap<bdd, formula, bdd_less_than>
-  expansion_simple(formula f, const bdd_dict_ptr& d, void *owner);
-
   SPOT_API expansion_t
   expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts);
 
-  SPOT_API formula
-  expansion_to_formula(expansion_t e, bdd_dict_ptr& d);
-
   SPOT_API twa_graph_ptr
   expand_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
 
   SPOT_API twa_graph_ptr
   expand_finite_automaton(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts);
+
+  SPOT_API formula
+  expansion_to_formula(expansion_t e, bdd_dict_ptr& d);
 }