remove_fin can trigger an assert in streett_to_generalized_buchi
@tmedioni, the Debian builds of next are failing core/ltl3dra.test
, and I suspect this is due to some of your recent changes. This test is skipped by most other builds because ltl3dra is not installed, so I'm not surprised the issue went unnoticed.
The file foo.hoa was generated with
% ltl3dra -f '!(<>((((p0) && (!(<>(p2)))) || ((!(p0)) && (<>(p2)))) U ((((p0) && (!(<>(p2)))) || ((!(p0)) && (<>(p2)))) && (<>(((p0) && (!([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3))))))))))))' | bin/autfilt --complement | fmt > foo.hoa
the failure can be reproduced with
% bin/autfilt --remove-fin foo.hoa
autfilt: streett_to_generalized_buchi() should only be called on automata with Streett-like acceptance
Could you have a look?