diff --git a/src/tests/safra.cc b/src/tests/safra.cc
new file mode 100644
index 000000000..7700136be
--- /dev/null
+++ b/src/tests/safra.cc
@@ -0,0 +1,40 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2015 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include <iostream>
+
+#include "twaalgos/safra.hh"
+#include "hoaparse/public.hh"
+#include "twaalgos/dotty.hh"
+
+
+int main(int argc, char* argv[])
+{
+  if (argc <= 1)
+    return 1;
+  char* input = argv[1];
+  spot::hoa_parse_error_list pel;
+  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::dotty_reachable(std::cout, res);
+}
diff --git a/src/tests/safra.test b/src/tests/safra.test
new file mode 100755
index 000000000..5e5241b71
--- /dev/null
+++ b/src/tests/safra.test
@@ -0,0 +1,102 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2015 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+. ./defs
+set -e
+
+cat >input.hoa << EOF
+HOA: v1
+name: "F\"x > 1\""
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0] 0 {0}
+[0] 1
+State: 1
+[1] 1
+[0] 0
+--END--
+EOF
+
+cat >out.exp << EOF
+digraph G {
+  rankdir=LR
+  node [shape="circle"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="a"]
+  1 [label="1"]
+  1 -> 2 [label="a\n{0}"]
+  1 -> 3 [label="b\n{3}"]
+  2 [label="2"]
+  2 -> 1 [label="a"]
+  2 -> 3 [label="b"]
+  3 [label="3"]
+  3 -> 3 [label="b"]
+  3 -> 0 [label="a"]
+}
+EOF
+
+run 0 ../safra input.hoa > out.dot
+diff out.dot out.exp
+
+cat >input.hoa << EOF
+HOA: v1
+name: "F\"x > 1\""
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[0] 0
+[0] 1
+State: 1
+[1] 1 {0}
+[0] 0
+--END--
+EOF
+
+cat >out.exp << EOF
+digraph G {
+  rankdir=LR
+  node [shape="circle"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="a"]
+  1 [label="1"]
+  1 -> 1 [label="a"]
+  1 -> 2 [label="b\n{0}"]
+  2 [label="2"]
+  2 -> 2 [label="b\n{0}"]
+  2 -> 0 [label="a"]
+}
+EOF
+
+run 0 ../safra input.hoa > out.dot
+diff out.dot out.exp