diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 4df94a77d..630ed12f5 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -669,6 +669,9 @@ int
 main(int argc, char **argv)
 {
   return protected_main(argv, [&] {
+      extra_options.set("simul", 0);
+      extra_options.set("det-simul", 0);
+      extra_options.set("tls-impl", 1);
       const argp ap = { options, parse_opt, nullptr,
                         argp_program_doc, children, nullptr, nullptr };
       if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index d677cf6fc..8a0d10a6c 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -23,50 +23,62 @@
 set -e
 
 cat >exp <<EOF
-parity 17;
+parity 18;
 0 1 0 1,2 "INIT";
 2 1 1 3;
 3 2 0 4,5;
-5 1 1 3,6;
-6 3 0 4,5;
-4 1 1 7,8;
-8 1 0 9,10;
-10 1 1 11,12;
-12 1 0 9,10;
-9 3 1 3,6;
-11 2 0 9,10;
-7 1 0 13,14;
-14 1 1 7,11;
-13 2 1 3,6;
-1 1 1 3,15;
-15 1 0 2,1;
+5 1 1 6,7;
+7 1 0 8,9;
+9 1 1 10,11;
+11 1 0 8,12;
+12 1 1 10,11;
+10 2 0 8,9;
+8 3 1 3,13;
+13 3 0 4,5;
+4 1 1 3,13;
+6 2 0 14,15;
+15 2 1 3,13;
+14 1 1 10,16;
+16 1 0 14,15;
+1 1 1 3,6;
 EOF
 ltlsynt --ins=a --outs=b -f 'GFa <-> GFb' --print-pg >out
 diff out exp
 
 cat >exp <<EOF
 REALIZABLE
-aag 23 1 2 1 16
+aag 30 1 3 1 26
 2
-4 3
-6 45
-47
-8 5 7
-12 2 8
-14 4 7
-16 2 14
-20 5 6
-22 3 20
-24 2 20
-26 4 6
-28 2 26
-30 3 26
-36 17 23
-38 13 36
-40 29 31
-42 25 40
-44 38 42
-46 25 29
+4 47
+6 57
+8 59
+61
+10 3 5
+12 7 9
+14 10 12
+16 2 5
+18 16 12
+20 3 4
+22 20 12
+24 2 4
+26 24 12
+28 6 9
+30 16 28
+32 10 28
+34 24 28
+36 20 28
+38 7 8
+40 16 38
+42 10 38
+44 23 33
+46 15 44
+48 27 31
+50 19 48
+52 35 41
+54 33 52
+56 50 54
+58 37 43
+60 48 54
 i0 a
 o0 b
 EOF
@@ -107,7 +119,7 @@ automaton has 3 states and 2 colors
 split inputs and outputs done in X seconds
 automaton has 9 states
 determinization done
-DPA has 14 states, 4 colors
+DPA has 12 states, 4 colors
 simplification done
 DPA has 11 states
 determinization and simplification took X seconds
@@ -124,7 +136,7 @@ automaton has 3 states and 4 colors
 simplification done in X seconds
 DPA has 3 states
 split inputs and outputs done in X seconds
-automaton has 9 states
+automaton has 8 states
 parity game built in X seconds
 parity game solved in X seconds
 EOF
@@ -268,3 +280,44 @@ for i in 2 3 4 5 6 10; do
     autfilt --remove-ap="$OUT" res$i | autfilt --dualize | autfilt --is-empty -q
   done
 done
+
+cat >exp <<EOF
+REALIZABLE
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "p0"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[t] 1
+State: 1
+[t] 2
+State: 2
+[!0] 2
+--END--
+EOF
+ltlsynt -x tls-impl=0 -f '!XXF(p0 & (p0 M Gp0))' > out
+diff out exp
+
+cat >exp <<EOF
+REALIZABLE
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "p0"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+--BODY--
+State: 0
+[!0] 0
+--END--
+EOF
+ltlsynt -x tls-impl=1 -f '!XXF(p0 & (p0 M Gp0))' > out
+diff out exp
+
+ltlsynt -f '!XXF(p0 & (p0 M Gp0))' > out
+diff out exp