Dear spot Team, I think I have found a bug in the emptiness checker of spot. When I use the following automation: HOA: v1 States: 8 Start: 0 Start: 1 AP: 0 acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) --BODY-- State: 0 {0} [(t)] 2 [(t)] 3 State: 1 {0} [(t)] 4 [(t)] 5 State: 2 {0} [(t)] 2 [(t)] 3 State: 3 {0} [(t)] 6 [(t)] 7 State: 4 {1} [(t)] 4 [(t)] 5 State: 5 {1} [(t)] 6 [(t)] 7 State: 6 [(t)] 6 [(t)] 7 State: 7 [(t)] 6 [(t)] 7 --END-- And invoke "autfilt --is-empty aut.hoa” (where aut.hoa contains the above automaton) I get the following error: autfilt: print_hoa(): automaton has transition-based acceptance despite prop_state_acc()==true This seems to be related to a similar bug that was fixed in version 2.7.1, so should (hopefully) be easy to fix. I used version 2.11.3 on a MacBook Pro with M1 Pro CPU. All the best, Raven