We are happy to announce the release of Spot 2.16.1 This is a maintenance releases fixings several bugs that have been reported since the release of 2.16. (But these bugs are actually much older.) This release contains contributions by Ondřej Lengál and myself. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.16.1.tar.gz See https://spot.lre.epita.fr/ for documentation and installation instructions. Please direct any feedback to <spot@lrde.epita.fr>, or create issues on https://gitlab.lre.epita.fr/spot/spot/-/works_item/new New in spot 2.16.1 (2026-10-16) Bug fixes: - is_generalized_rabin() and is_generalized_streett() could fail on acceptance formulas that use the maximum number of colors supported by Spot. - writing to files using `-o PATTERN.out` will now flush after each formula or automaton is output. This ensure that the file can be properly read even if the tool hasn't yet closed it (because it might append to it later). - Some algorithms that temporarily override the acceptance condition of an automaton (via scc_and_mark_filter) could lower the number of acceptance sets declared by that automaton when restoring its acceptance condition, if the highest sets occurred only on edges. For instance, autfilt --is-inherently-weak, --is-semi-deterministic, or --is-unambiguous could output automata that use undeclared acceptance sets, and that could not be parsed back. (Issue #655.) - autfilt --track-formula could crash on exit when Spot was built with static libraries, because the formula it kept in a global variable was destroyed after the table of atomic propositions. (Issue #656.) - When called with acc_clean and propagate_col disabled, to_parity() could produce an automaton with a different language if some edges of its input carried acceptance sets that are not used by the acceptance condition. It also read past the end of an internal array in that case. (Issue #657.) - to_parity() failed an assertion in try_parity_prefix() when the SCCs left after removing a parity prefix produced no colored edge. The code following that assertion was already correct in that case, but only by relying on unsigned wrap-around. (Issue #658.) - to_parity() failed an assertion when no edge of its output received a color although its input had edges, which happens when all cycles of the input are rejecting (e.g., with acceptance "f"). Such automata are now converted into automata with acceptance "f". (Issue #659.) - Improve speed of syntactic implication checks. (Issue #660.) - Translation from LTL to automata with generic acceptance conditions (e.g., with `ltl2tgba G -D`) could produce an incorrect automaton on formula involving <-> or xor, with a safety formula in one operand, and some non-obligation formula on the other one. (Issue #662.)