Announcing Kind 2 2.1.1

[kind2-announce]

Dear all,

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

This release includes multiple improvements and bug fixes. Notably:

- Add a new option for printing the set of viable states of a realizable contract (`--print_viable_states`).
- Allow the second argument of a shift operator to be non-constant.
- Allow variables with subrange types in the interface of a contract node.
- Add support for the latest versions of SMT solver Bitwuzla (v0.1.1 and above).
- Accept new versions of cvc5 for proof production (up to 1.1.0).
- Fix soundness bug in IC3IA engine.
- Fix compatibility issue with OCaml 5.0.0+
- Fix printing of values of stateless variables in counterexamples (bug introduced in v2.0.0).
- Fix several bugs related to the definition and use of arrays in Lustre models.
- Add static checks on the definition of global subrange constants.
- Accept the `param` keyword for the declaration of system parameters (global constants without a definition).
- Add subrange and enum constraints on system parameters.
- Fix type checking and handling of constant node arguments.
- Other improvements and bug fixes in the Lustre front end.

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