Dafny 3.9.1

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)

Bug fixes

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