In addition to several improvements and bug fixes, this release includes the following new functionalities:
- New map and set types.
- Support for structural equality for arrays, maps, and sets.
- Bottom-up type inference for polymorphic node and function calls (using base types only).
- New syntax for specifying contracts.
- New type ascription operator.
- New conditional expression and blocks with lazy semantics, and short-circuiting versions of 'and', 'or', and '=>'.
- Support for machine integers of arbitrary concrete size, including generation of invariant candidates.
- New built-in operator choose. Like
any, it denotes an arbitrary stream of values, but the value is determined by the free variables in the predicate (behaving like a function). - Support for subranges with symbolic constant bounds.
- Support for quantifiers in refinement type predicates.
- Support for a concise refinement type syntax for quantified variables (e.g.
forall (i: int | i > 0)). - New safety proof production feature based on the new cvc5 CPC proof format (replaces LFSC); compatible with cvc5 1.3.2.
- Support for Bitwuzla as an interpolating solver.
- New contract monitor feature to check a given trace satisfies a contract.
- Verification of constant definitions and realizability checks of free constants (a.k.a system parameters) with refinement types (see documentation for more details).
Please refer to the CHANGES file for a more detailed description and a list of breaking changes, and to the user documentation for more details.