diff --git a/doc/org/satmin.org b/doc/org/satmin.org
index da9eedf25..eb137ae75 100644
--- a/doc/org/satmin.org
+++ b/doc/org/satmin.org
@@ -162,17 +162,17 @@ digraph G {
0 -> 0 [label=]
0 -> 1 [label=]
0 -> 2 [label=]
- 1 [label="1"]
- 1 -> 4 [label=⓿>]
- 1 -> 5 [label=⓿>]
+ 1 [label="1", peripheries=2]
+ 1 -> 4 [label=]
+ 1 -> 5 [label=]
2 [label="2"]
2 -> 1 [label=]
2 -> 4 [label=]
2 -> 5 [label=]
- 3 [label="3"]
- 3 -> 0 [label=⓿>]
- 3 -> 1 [label=⓿>]
- 3 -> 2 [label=⓿>]
+ 3 [label="3", peripheries=2]
+ 3 -> 0 [label=]
+ 3 -> 1 [label=]
+ 3 -> 2 [label=]
4 [label="4"]
4 -> 0 [label=]
4 -> 1 [label=]
diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index fefff6535..cb47abaa9 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -639,6 +639,8 @@ namespace spot
auto a = make_tgba_digraph(autdict);
a->copy_ap_of(aut);
acc_cond::mark_t acc = a->set_single_acceptance_set();
+ if (state_based)
+ a->prop_state_based_acc();
a->new_states(satdict.cand_size);
unsigned last_aut_trans = -1U;
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 1798a91ff..230a67f62 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -780,7 +780,8 @@ namespace spot
auto a = make_tgba_digraph(autdict);
a->copy_ap_of(aut);
a->set_generalized_buchi(satdict.cand_nacc);
-
+ if (state_based)
+ a->prop_state_based_acc();
a->new_states(satdict.cand_size);
// Last transition set in the automaton.
diff --git a/src/tgbatest/satmin2.test b/src/tgbatest/satmin2.test
index 5e37d3475..b8a0cacaf 100755
--- a/src/tgbatest/satmin2.test
+++ b/src/tgbatest/satmin2.test
@@ -57,3 +57,9 @@ EOF
../ltl2tgba -RS1 -kt -XH input.hoa > output
diff output expected
+
+# At some point, this formula was correctly minimized, but
+# the output was not marked as state-based.
+../../bin/ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out
+grep 'properties:.*state-acc' out
+grep 'properties:.*deterministic' out