New features
-
Add a check to
dafny runthat notifies the user when a value that was parsed as a user program argument, and which occurs before a--token, starts with--, since this indicates they probably mistyped a Dafny option name. (#5097) -
Add an option --progress that can be used to track the progress of verification. (#5150)
-
Add the attribute
{:isolate_assertions}, which does the same as{:vcs_split_on_every_assert}. Deprecated{:vcs_split_on_every_assert}(#5247)
Bug fixes
-
(soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap (#4844)
-
Add uniform checking of type characteristics in refinement modules (#5146)
-
Fixed links associated with the standard libraries. (#5176)
-
fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits.
feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields.
(#5234) -
Fix the default string value emitted for JavaScript (#5239)