Announcing Kind 2 1.5.1

[kind2-announce]

Dear all,

We are happy to announce a new minor release (v1.5.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:

- Improve performance of realizability checks with Z3.
- Fix realizability check of imported functions.
- Fix realizability check when `--ae_val_use_ctx` is false.
- Fix generation of tracing information when a contract is proven unrealizable.
- Fix shape of generated invariant candidates when `--invgen_all_out` is true.
- Fix generation of SMT-LIB 2 certificates.
- Make Kind 2 compatible with the latest version of the OCaml bindings for ZMQ.

In addition, this version adds support for a new VS Code extension for Kind 2:
https://marketplace.visualstudio.com/items?itemName=kind2-mc.vscode-kind2

We thank Andreas Katis for his feedback and bug reports.

Please refer to the CHANGES document [2] for a more detailed
description, and to the user's documentation [3] for further 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.
It can also be installed through OPAM.

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.5.1/CHANGES.md
[3] https://kind.cs.uiowa.edu/kind2_user_doc/