dafny-lang/dafny v3.9.1 on GitHub

New features

The language server now supports all versions of z3 ≥ 4.8.5. Dafny is still distributed with z3 4.8.5 and uses that version by default. (#2820)

Correct error highlighting on function called with default arguments (#2826)
Crash in the LSP in some code that does not parse (#2833)
A function used as a value in a non-ghost context must not have ghost parameters, and arrow types cannot have ghost parameters. (#2847)
Compiled lambdas now close only on non-ghost variables (#2854)
Previously, for a file printing the number of arguments, dafny printing.dfy -compileTarget:js --args 1 2 3 would print 4: one for the executable, one for each argument.
But dafny -compile:2 -compileTarget:js printing.dfy; node ./printing.js would print 5: One for node, one for ./printing.js, and one for each argument.
This fix ensures that node ./printing.js is considered as a single argument, and the first argument, to be consistent with every other language.
(#2876)
Handle sequence-to-string equality correctly in the JavaScript runtime (#2877)
don't crash on type synonyms and subset types of array types in LHSs of simultaneous assignments (#2884)
Removed an bogus optimization on the Language Server (#2890)
The Dafny-to-Java compiler will now fully-qualify type casts in pattern destructors, avoiding "reference to TYPE is ambiguous" errors from javac. (#2904)
Variable declarations and formals in match cases do not trigger errors anymore. (#2910)