Announcing Kind 2 1.3.1

[kind2-announce]

Dear all,

We are happy to announce a new minor release (v1.3.1) of Kind 2,
an open-source, multi-engine, SMT-based automatic model checker for
safety properties of Lustre programs [1].

This release includes performance improvements and various fixes. Notably:

- It fixes a soundness issue in path compression when there are temporal dependencies
  between input values. (Thank you to M. Anthony Aiello for finding this bug).
- It fixes a bug in the extraction of an active path during IC3 generalization.
- It improves IC3 performance over large models that contain reals or machine integers.
- It fixes an issue reading models from the latest version of Z3 (4.8.10).
  The issue caused a runtime error during IVC generation.

Please see the CHANGES document [2] and the user's documentation [3] for more details.

The latest version of Kind 2 can be downloaded from
https://github.com/kind2-mc/kind2/releases and is distributed in
source form, as well as binaries for both Linux and macOS.

Feedback and feature requests are most welcome. Please contact the
developers or open an issue directly on Github at
https://github.com/kind2-mc/kind2/issues/new

If you want to participate in discussions with developers and other
users of Kind 2, you are encouraged to join the kind2-users group at
https://groups.google.com/d/forum/kind2-users

Best,

The Kind 2 Development Team

[1] http://kind.cs.uiowa.edu
[2] https://github.com/kind2-mc/kind2/blob/v1.3.1/CHANGES.md
[3] https://kind.cs.uiowa.edu/kind2_user_doc/