diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc
index 97a2eceb3..ed9ad7d06 100644
--- a/spot/twaalgos/ltl2tgba_fm.cc
+++ b/spot/twaalgos/ltl2tgba_fm.cc
@@ -107,7 +107,7 @@ namespace spot
     {
       typedef twa_graph::namer<formula> namer;
     public:
-      ratexp_to_dfa(translate_dict& dict);
+      ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming = false);
       std::tuple<const_twa_graph_ptr, const namer*, const state*>
       succ(formula f);
       ~ratexp_to_dfa();
@@ -122,6 +122,7 @@ namespace spot
       typedef robin_hood::unordered_node_map<formula, labelled_aut> f2a_t;
       std::vector<labelled_aut> automata_;
       f2a_t f2a_;
+      bool disable_scc_trimming_;
     };
 
     // Helper dictionary.  We represent formulae using BDDs to
@@ -907,8 +908,9 @@ namespace spot
     }
 
 
-    ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict)
+    ratexp_to_dfa::ratexp_to_dfa(translate_dict& dict, bool disable_scc_trimming)
       : dict_(dict)
+      , disable_scc_trimming_(disable_scc_trimming)
     {
     }
 
@@ -961,6 +963,12 @@ namespace spot
             }
         }
 
+      if (disable_scc_trimming_)
+        {
+          automata_.emplace_back(a, namer);
+          return labelled_aut(a, namer);
+        }
+
       // The following code trims the automaton in a crude way by
       // eliminating SCCs that are not coaccessible.  It does not
       // actually remove the states, it simply marks the corresponding
@@ -2222,7 +2230,7 @@ namespace spot
   }
 
   twa_graph_ptr
-  sere_to_tgba(formula f, const bdd_dict_ptr& dict)
+  sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming)
   {
     f = negative_normal_form(f);
 
@@ -2230,7 +2238,7 @@ namespace spot
     twa_graph_ptr a = make_twa_graph(dict);
 
     translate_dict d(a, s, false, false, false);
-    ratexp_to_dfa sere2dfa(d);
+    ratexp_to_dfa sere2dfa(d, disable_scc_trimming);
 
     auto [dfa, namer, state] = sere2dfa.succ(f);
 
diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh
index aa9bc1d1d..18341fb37 100644
--- a/spot/twaalgos/ltl2tgba_fm.hh
+++ b/spot/twaalgos/ltl2tgba_fm.hh
@@ -90,5 +90,5 @@ namespace spot
                  const output_aborter* aborter = nullptr);
 
   SPOT_API twa_graph_ptr
-  sere_to_tgba(formula f, const bdd_dict_ptr& dict);
+  sere_to_tgba(formula f, const bdd_dict_ptr& dict, bool disable_scc_trimming = false);
 }