dafny-lang/dafny v2.2.0 on GitHub

Version 2.2.0 differs over version 2.1.1 in the following ways:

Language

In abstract modules, const declarations are allowed to omit initializing expressions,
even if it is not known how to initialize values of its type.
Variables introduced in pattern-matching var statements are now mutable, like
other local variables.
Added general map comprehensions, of the form map x,y | R(x,y) :: f(x,y) := g(x,y).
This map takes f(x,y) to g(x,y), where x and y are any values that satisfy
R(x, y). The ordinary map comprehension map x | R(x) :: g(x) is a special case
of the general map comprehension map x | R(x) :: x := g(x).
Collection types (sets, sequences, multisets, and maps) and many varieties of
inductive datatypes are now considered as having a zero initializer. This includes
string, which is a synonym for seq<char>.
Syntactic heuristics for detecting finite sets consider equalities.
Possibly-null array-type names are now keywords (e.g., array?).
An expression of the form exists x :: A ==> B, which is almost always a mistakes,
now generates an warning. Use parentheses around the quantifier body to override.

New default encoding of non-linear arithmetic (/arith:1). Also added various
experimental modes (/arith switch) that are subject to change in the future.
Various bug fixes.

New /spillTargetCode modes 2 and 3, which write out the .cs file without
invoking the C# compiler
Turn off warning 0162 (unreachable code)
Fixed equalities-checking bug.