Dafny 3.9.1

[atomb]

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. (feat: Support for arbitrary versions of z3 #2820)

Bug fixes

• Correct error highlighting on function called with default arguments (Fix: Position of default argument to be at the call site, not definition #2826)

• Crash in the LSP in some code that does not parse (Crash of the language server #2833)

• A function used as a value in a non-ghost context must not have ghost parameters, and arrow types cannot have ghost parameters. (fix: A function with ghost parameters used as a value is ghost #2847)

• Compiled lambdas now close only on non-ghost variables (Fix: 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.
  (Fix: Node CLI arguments for dafny to have the right order #2876)

• Handle sequence-to-string equality correctly in the JavaScript runtime (fix: string-seq equality in JS runtime #2877)

• don't crash on type synonyms and subset types of array types in LHSs of simultaneous assignments (fix: expand array synonyms / subset types in LHS assignments #2884)

• Removed an bogus optimization on the Language Server (Language Server not stable anymore #2890)

• The Dafny-to-Java compiler will now fully-qualify type casts in pattern destructors, avoiding "reference to TYPE is ambiguous" errors from javac. (fix(java): unqualified type cast in pattern dtor #2904)

• Variable declarations and formals in match cases do not trigger errors anymore. (Fix: Variable declarations in match cases, formals do not trigger errors anymore #2910)

---

This discussion was created from the release Dafny 3.9.1.