Dafny 3.9.0

[cpitclaudel]

• feat: Support for testing certain contracts at runtime with a new /testContracts flag (Add plugin to create wrapper functions/methods to check contracts at runtime #2712)
• feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (Feat: Support for full UTF8 parsing by default. #2717)
• feat: Command-line arguments are now available from Main in Dafny programs, using Main(args: seq<string>) (feat: Dafny Main method to accept optional seq<string> argument #2594)
• feat: Generate warning when 'old' has no effect (feat: Generate a warning when 'old' has no effect #2610)
• fix: Missing related position in failing precondition (fix: Missing related position in failing precondition #2658)
• fix: No more IDE crashing on the elephant operator (Fix: No crash anymore on the IDE when using the elephant operator #2668)
• fix: Use the right comparison operators for bitvectors in Javascript (fix: Use the right >/</>=/<= comparison operators for bitvectors in JS #2716)
• fix: Retain non-method-body block statements when cloning abstract signatures (fix: retain non-method-body block statements when cloning abstract signatures #2731)
• fix: Correctly substitute variables introduced by a binding guard (Solution to issue 2265 related to erroneous substitution under bindin… #2745)
• fix: The CLI no longer attempts to load each DLL file passed to it. (chore: Factor out projects without runtimes #2568)
• fix: Improved hints and error messages regarding variance/cardinality preservation (Improve error messages about variance and cardinality preservation #2774)
• feat: New behavior for import opened M where M contains a top-level declaration M, see PR for a full description (feat!: New behavior for opened import where module contains homonymous top-level declaration #2355)
• fix: The DafnyServer package is now published to NuGet as well, which fixes the previously-broken version of the DafnyLanguageServer package. (Publish DafnyServer/Driver/Core to NuGet as well #2787)
• fix: Support for spaces in the path to Z3 (Fix: Support for Z3 solver path with spaces #2812)
• deprecate: Statement-level refinement syntax (e.g. assert ...) is deprecated (Deprecating statement refinement syntax - #2765 #2756)
• deprecate: The form of the modify statement with a block statement is deprecated
• docs: The user documentation at https://dafny.org has a new landing page

---

This discussion was created from the release Dafny 3.9.0.