bogus co-Büchi generation by nsa_to_nca

Consider the following dnf.hoa automaton with DNF acceptance:

It recognizes the persistence formula (FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb):

% ltl2tgba -f '(FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb)' > ref.hoa
% autfilt -c --equivalent-to ref.hoa dnf.hoa
1
% ltlfilt --format='%[v]h' -f '(FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb)'
persistence

and it does not accept the following word:

% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}'  dnf.hoa ref.hoa
0

(All runs for this word, starting with 0->1->3... or 0->2->6... ultimately cycle between states 6 and 8.)

Now let's build a (supposedly) equivalent NCA automaton:

python3 -c 'import spot; print(spot.dnf_to_nca(spot.automaton("dnf.hoa")).to_str())' > nca.hoa

That automaton is too big to be displayed, but it does accept the above word, which isn't expected.

% autfilt --stats=%s nca.hoa
69
% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}' nca.hoa
1
% autfilt -c --equivalent-to ref.hoa nca.hoa
0                                   

The DCA version is bogus as well (but that isn't surprising given that dnf_to_dca() calls dnf_to_nca() first), but it has the advantage of being simplifiable to some automaton small enough to be displayed. This allows us to double-check that the given word is really accepted; i.e., this is probably not a bug of remove_fin() (used by --accept-word and --equivalent-to).

% python3 -c 'import spot; print(spot.dnf_to_dca(spot.automaton("dnf.hoa")).to_str())' | autfilt --small > dca.hoa
% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}' dca.hoa
1

The accepting run is 0->1->6->13->4->7->4->7->4->....

I have also tested that the output of dnf_to_streett is equivalent to the reference, so the problem comes after that.

% python3 -c 'import spot; print(spot.dnf_to_streett(spot.automaton("dnf.hoa")).to_str())' > streett.hoa
% autfilt -c --equivalent-to streett.hoa ref.hoa
1