Skip to content

Issues: dafny-lang/dafny

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

1,009 Open 1,582 Closed
1,009 Open 1,582 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Unstable CLI test git-issues/git-issue-697j.dfy, related to Rust backend kind: language development speed Slows down development of Dafny the language, flaky tests
#5537 opened Jun 6, 2024 by keyboardDrummer
1
Costless by clause in assert .. by { } when using --isolate-assertions
#5536 opened Jun 6, 2024 by keyboardDrummer
2
Verification hang apparently caused by Std import kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5534 opened Jun 6, 2024 by nverhaaren
1
Issue with multi-backend-testing kind: language development speed Slows down development of Dafny the language, flaky tests
#5533 opened Jun 5, 2024 by MikaelMayer
Bad encoding for this in tail recursive functions when compiling to Java during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: java Dafny's Java transpiler and its runtime
#5532 opened Jun 5, 2024 by fabiomadge
assertion of map values fails when same postcondition succeeds (or if preceded by Keys assertion) incompleteness Things that Dafny should be able to prove, but can't kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: verifier Translation from Dafny to Boogie (translator)
#5527 opened Jun 5, 2024 by kjx
2
Verification ignores resource limits kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5525 opened Jun 4, 2024 by hmijail
3
Constraint-less newtypes assumed to be nonempty during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5521 opened Jun 3, 2024 by RustanLeino
1
@RustanLeino
Base type throws off witness checking during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#5520 opened Jun 3, 2024 by RustanLeino
1
@RustanLeino
Flaky test: ConcurrentCompilationDoesNotBreakCaching kind: language development speed Slows down development of Dafny the language, flaky tests
#5515 opened May 31, 2024 by MikaelMayer
Unstable test ChangeAndUndoProjectWithMultipleFiles kind: language development speed Slows down development of Dafny the language, flaky tests
#5510 opened May 30, 2024 by keyboardDrummer
@keyboardDrummer
3
Confusing type error due to missing path qualifier kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#5505 opened May 29, 2024 by mschlaipfer
Integration tests getting really slow kind: language development speed Slows down development of Dafny the language, flaky tests
#5499 opened May 28, 2024 by robin-aws
Incorrect multiplication in Dafny: Show Counterexample incompleteness Things that Dafny should be able to prove, but can't kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: counterexamples Counterexample generation
#5490 opened May 25, 2024 by cdstanford
4
Instable test: "DafnyTestGeneration.Test" test run gets cancelled, possibly due to taking too long kind: language development speed Slows down development of Dafny the language, flaky tests
#5488 opened May 24, 2024 by keyboardDrummer
4
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5486 opened May 23, 2024 by aws-crypto-tools-ci-bot
14
[PRERELEASE REGRESSION] Dafny prerelease regression from smithy-lang/smithy-dafny breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5485 opened May 23, 2024 by dafny-lang-bot
9
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-cryptographic-material-providers-library breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5473 opened May 21, 2024 by aws-crypto-tools-ci-bot
13
Stack overflow with long-ish seq kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#5471 opened May 21, 2024 by hmijail
5
Guidance on z3 versions? kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: documentation Dafny's reference manual, tutorial, and other materials
#5470 opened May 21, 2024 by hmijail
1
Compiled code has useless duplicate membership test area: performance Performance issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#5465 opened May 20, 2024 by MikaelMayer
[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb breaking-change Any change that will cause existing Dafny codebases to break (excluding verification instability)
#5462 opened May 17, 2024 by robin-aws
Flaky test: LanguageServer.IntegrationTest.Lookup.SignatureHelpTest.SignatureHelpOnOpeningParenthesesReturnsSignatureOfClosestFunction kind: language development speed Slows down development of Dafny the language, flaky tests
#5460 opened May 17, 2024 by MikaelMayer
2
Flaky Test: LanguageServer.IntegrationTest.Lookup.DocumentSymbolTest.CanResolveSymbolsForMultiFileProjects kind: language development speed Slows down development of Dafny the language, flaky tests
#5443 opened May 14, 2024 by MikaelMayer
@keyboardDrummer
2
Unstable test ChangingTheDocumentStopsOnChangeVerification kind: language development speed Slows down development of Dafny the language, flaky tests
#5436 opened May 14, 2024 by keyboardDrummer
@keyboardDrummer
1
ProTip! Adding no:label will show everything without a label.