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

Clear current search query, filters, and sorts
1,020 Open 1,592 Closed
1,020 Open 1,592 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
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

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
Issue with multi-backend-testing kind: language development speed Slows down development of Dafny the language, flaky tests priority: not yet Will reconsider working on this when we're looking for work
#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 priority: not yet Will reconsider working on this when we're looking for work
#5532 opened Jun 5, 2024 by fabiomadge
1
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) priority: not yet Will reconsider working on this when we're looking for work
#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 part: z3 Issue is in Z3 priority: not yet Will reconsider working on this when we're looking for work
#5525 opened Jun 4, 2024 by hmijail
6
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
Unstable test ChangeAndUndoProjectWithMultipleFiles kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#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
Unstable 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 priority: next Will consider working on this after in progress work is done
#5488 opened May 24, 2024 by keyboardDrummer
@robin-aws
9
[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
36
Export sets should transitively consider subset types kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done
#5417 opened May 9, 2024 by MikaelMayer
@MikaelMayer
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
2
Flaky test: LanguageServer.IntegrationTest.Lookup.SignatureHelpTest.SignatureHelpOnOpeningParenthesesReturnsSignatureOfClosestFunction kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#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 priority: next Will consider working on this after in progress work is done
#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 priority: next Will consider working on this after in progress work is done
#5436 opened May 14, 2024 by keyboardDrummer
@keyboardDrummer
2
strange assertion failure incompleteness Things that Dafny should be able to prove, but can't
#5435 opened May 14, 2024 by toNanjingnan
2
Flaky LSP test: DocumentAddedToExistingProjectDoesNotCrash kind: language development speed Slows down development of Dafny the language, flaky tests part: language server Support for LSP in Dafny (server part; client is in ide-vscode repo) priority: next Will consider working on this after in progress work is done
#5434 opened May 13, 2024 by MikaelMayer
1
@keyboardDrummer
7
Prover died on simple program during 1: program development Bad error message or documentation; IDE bug; crash compiling invalid program kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#5421 opened May 10, 2024 by MikaelMayer
2
Flaky CI Test: LanguageServer.IntegrationTest.ProjectFiles.CompetingProjectFilesTest.ProjectFileDoesNotOwnAllSourceFilesItUses kind: language development speed Slows down development of Dafny the language, flaky tests priority: next Will consider working on this after in progress work is done
#5420 opened May 10, 2024 by MikaelMayer
@keyboardDrummer
11
Standard Library: Parser combinators part: standard libraries Standard libraries packaged in the Dafny distribution
#5418 opened May 9, 2024 by robin-aws
1
ProTip! What’s not been updated in a month: updated:<2024-05-26.