dafny-lang/dafny v3.13.0

Dafny 3.13.0

on GitHub

New features

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

Bug fixes

• Fix translation of Dafny FunctionHandles to Boogie (#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. (#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
    (#3641)