Dafny 3.13.0

[jtristan]

New features

• Expose non-relaxed definite assignment (/definiteAssignment:4) in legacy CLI (Improve definite assignment 4 #3641)

Bug fixes

• Fix translation of Dafny FunctionHandles to Boogie (fix: Fix naming of formals in Translator #2266)

• To ensure that a class correctly implements a trait, we perform an override check. This check was previously faulty across modules, but works unconditionally now. (fix: Override checks with canCall precondition  #3479)

• Fixes to definite assignment and determinism options:

  • --enforce-determinism now forbids constructor-less classes
  • With non-relaxed definite assignment, allow auto-init fields to be uninitialized
    (Improve definite assignment 4 #3641)

---

This discussion was created from the release Dafny 3.13.0.