[release] 0.25.8

[apalache-bot]

Reviewer instructions

• Check the changelog to ensure the version increment is consistent with https://semver.org/.
  • If a different version should be released, follow the instructions.
• Review the changeset as a sanity check.
• Approve the PR, if it pases muster.
• Merge this branch (do not squash or rebase), but DO NOT DELETE THE BRANCH.
• After the release has been published to github, delete this branch.

---

Release notes

0.25.8 - 2022-07-04

Features

• Add support for temporal properties, enabled via the --temporal flag, see Read temporal formulas with Spec+--temporal rather than Next+Init+--inv #1815
• Support variants in the model checker with --features=rows, see Support for variants in the model checker #1870
• serialize variants to the ITF format, see fix ITF output for variants #1898
• Annotate counterexample traces to improve readability of temporal properties, see Make counterexample writer more informative #1823
• Replace PostTypeChecker pass with an additional predicate, see Remove PostTypeChecker #1878

Bug fixes

• Add support for checking temporal properties with primed expressions inside, see Add support for actions under temporal operators #1879
• Fixed inlining of nullary polymorphic operators, see Type concretization for nullary expressions #1880
• Fix crash with infinite sets in the arrays encoding, see Encode infinite sets in the arrays encoding #1802