We are happy to announce the release of Spot 2.16.2 This is a maintenance release fixing a bug in the on-the-fly LTL satisfiability solver, introduced in version 2.16. You can find the new release here: http://www.lre.epita.fr/dload/spot/spot-2.16.2.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.2 (2026-11-03) Library: - The "simplifier" argument of ltl_to_tgba_fm(), and the equivalent argument of the ltl_to_tgba_fm_otf() constructor, are deprecated. When given, that simplifier used to simplify the formula representing each state of the automaton before computing its successors, but this is unsound in general, and was not used by Spot in practice, except for the recent otf_satisfiable() addition. The argument is now only used to simplify the input formula, and will be removed in a future release. (Issue #663.) Bug fixes: - ltl_satisfiable() could report an unsatisfiable formula as satisfiable, e.g., G(b -> XXd) & Gb & FG!d, because the on-the-fly explorer it uses was built with a simplifier; see the deprecation above. (Issue #663.)