Dafny 2.2.0

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.

Verifier

• 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.

Compiler

• 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.

Miscellaneous

• Improvements in Linux and MacOS run script

• Various bug fixes