diff --git a/src/tests/safra.cc b/src/tests/safra.cc
index 7700136be..01d25e661 100644
--- a/src/tests/safra.cc
+++ b/src/tests/safra.cc
@@ -18,23 +18,43 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <iostream>
+#include <cstring>
 
+#include "twa/twagraph.hh"
 #include "twaalgos/safra.hh"
+#include "twaalgos/translate.hh"
 #include "hoaparse/public.hh"
+#include "ltlparse/public.hh"
 #include "twaalgos/dotty.hh"
 
 
 int main(int argc, char* argv[])
 {
-  if (argc <= 1)
+  if (argc <= 2)
     return 1;
-  char* input = argv[1];
-  spot::hoa_parse_error_list pel;
+  char* input = argv[2];
   auto dict = spot::make_bdd_dict();
-  auto aut = spot::hoa_parse(input, pel, dict);
-  if (spot::format_hoa_parse_errors(std::cerr, input, pel))
-    return 2;
-  auto res = tgba_determinisation(aut->aut);
+  spot::twa_graph_ptr res;
+  if (!strncmp(argv[1], "-f", 2))
+    {
+      spot::ltl::parse_error_list pel;
+      const spot::ltl::formula* f =
+      spot::ltl::parse(input, pel, spot::ltl::default_environment::instance(),
+                       false);
+      spot::translator trans(dict);
+      trans.set_pref(spot::postprocessor::Deterministic);
+      auto tmp = trans.run(f);
+      res = spot::tgba_determinisation(tmp);
+      f->destroy();
+    }
+  else if (!strncmp(argv[1], "--hoa", 5))
+    {
+      spot::hoa_parse_error_list pel;
+      auto aut = spot::hoa_parse(input, pel, dict);
+      if (spot::format_hoa_parse_errors(std::cerr, input, pel))
+        return 2;
+      res = tgba_determinisation(aut->aut);
+    }
 
   spot::dotty_reachable(std::cout, res);
 }
diff --git a/src/tests/safra.test b/src/tests/safra.test
index 5e5241b71..14cbbda06 100755
--- a/src/tests/safra.test
+++ b/src/tests/safra.test
@@ -60,7 +60,7 @@ digraph G {
 }
 EOF
 
-run 0 ../safra input.hoa > out.dot
+run 0 ../safra --hoa input.hoa > out.dot
 diff out.dot out.exp
 
 cat >input.hoa << EOF
@@ -98,5 +98,5 @@ digraph G {
 }
 EOF
 
-run 0 ../safra input.hoa > out.dot
+run 0 ../safra --hoa input.hoa > out.dot
 diff out.dot out.exp
diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc
index 4153e65a4..6d9acb02f 100644
--- a/src/twaalgos/safra.cc
+++ b/src/twaalgos/safra.cc
@@ -20,6 +20,7 @@
 #include <deque>
 
 #include "safra.hh"
+#include "twaalgos/degen.hh"
 
 namespace spot
 {
@@ -44,7 +45,6 @@ namespace spot
                 res.emplace_back(safra_state(nb_braces_.size()), t.cond);
               }
             safra_state& ss = res[idx].first;
-            assert(ss.nb_braces_.size() == ss.is_green_.size());
             ss.update_succ(node.second, t.dst, t.acc);
             assert(ss.nb_braces_.size() == ss.is_green_.size());
           }
@@ -150,6 +150,8 @@ namespace spot
     // TODO handle multiple accepting sets
     if (acc.count())
       {
+        assert(acc.has(0) && acc.count() == 1 &&
+               "Only one TBA are accepted at the moment");
         // Accepting transition generate new braces: step A1
         copy.emplace_back(nb_braces_.size());
         // nb_braces_ gets updated later so put 0 for now
@@ -227,8 +229,13 @@ namespace spot
   }
 
   twa_graph_ptr
-  tgba_determinisation(const const_twa_graph_ptr& aut)
+  tgba_determinisation(const const_twa_graph_ptr& a)
   {
+    const_twa_graph_ptr aut;
+    if (a->acc().is_generalized_buchi())
+      aut = spot::degeneralize_tba(a);
+    else
+      aut = a;
     auto res = make_twa_graph(aut->get_dict());
     res->copy_ap_of(aut);
     res->prop_copy(aut,