• fix: Use the right bitvector comparison in decrease checks
  (#2512)
• fix: Don't use native division and modulo operators for non-native int-based newtypes in Java and C#.
  (#2416)
• feat: Dafny now supports disjunctive (“or”) patterns in match statements and expressions. Cases are separated by | characters. Disjunctive patterns may not appear within other patterns and may not bind variables.
  (#2448)
• feat: The Dafny Language Server used by the VSCode IDE extension is now available as a NuGet package called DafnyLanguageServer (#2600)
• fix: Counterexamples - fix an integer parsing bug and correctly extract datatype and field names (#2461)
• feat: New option -diagnosticsFormat:json to print Dafny error messages as JSON objects (one per line).
  (#2363)
• fix: No more exceptions when hovering over variables without type, and types of local variabled kept under match statements (#2437)
• fix: Check extreme predicates and constants in all types, not just classes
  (#2515)
• fix: Correctly substitute type variables in override checks
  (#2522)
• feat: predicate P(x: int): (y: bool) ... is now valid syntax (#2454)
• fix: Improve the performance of proofs involving bit vector shifts (#2520)
• fix: Perform well-definedness checks for ensures clauses of forall statements (#2606)