Repository Issue Activity (beta)

#6481 verification regression between mid March & early June

#5640 [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb

#5486 [PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny

#6528 [severity: wash your dog first] Dafny error message about missing z3 is slightly wrong

#6345 Crash when named class constructor is used inside match case

#6523 soundness bug 2

#6522 soundness bug 1

#6512 C++ backend gives wrong values for bv8/bv16 arithmetic (not truncated to width)

#6511 Question about Dafny's use of Boogie

#3031 Enable running `dafny verify` and `dafny server` in the browser

#6503 Unhandled exception: System.NullReferenceException on introduction of `var v :| ...; `

#6505 --cores:<XX>% is parsed with the ambient culture, so a fractional percentage can silently mean something else

#6504 dafny run --coverage-report leaves two temporary files behind per invocation

#6491 Java: collections assume default behavior of `equals()`, `hashCode()`

#6499 Datatype with an {:extern} member resolves and verifies but emits uncompilable code on every backend

#5335 Enable safely using doo files that were verified against other doo files

#6486 Diamond dependencies lead to "Duplicate module name" error when building `.doo` library without sufficent usage of `--library`

#6479 Success of verification of bitvectors depends on unused function argument

#6485 Missing `FileIO` in `.doo` builds

#6476 On linux, `dafny verify file.dfy` verifies both `file.dfy` and `File.dfy`, ignoring the case difference

#6475 Boogie model parser fails on locales with non-period decimal separator (breaks dafny verify counterexamples and dafny generate-tests)

#6470 latest nightly doesn't support read clauses referring to fields in traits (see also https://github.com/dafny-lang/ide-vscode/issues/556)

#6472 Standalone language server installation fails for VS Code extension 3.5.3 on MacOS

#6343 Soundness issue when variable present in function postcondition with recursive call with same arguments

#6440 `TypeDescriptor.newArray()` uses reflection to create arrays — incompatible with GraalVM native-image