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