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 Open 11 Closed
1 Open 11 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

Let bindings may cause invalid triggers that Z3 rejects 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) priority: not yet Will reconsider working on this when we're looking for work
#4409 opened Aug 10, 2023 by Chris-Hawblitzel
1
Compiled code initializes datatype fields with wrong default values kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
#610 by Chris-Hawblitzel was closed Nov 24, 2020 Dafny 3.0
1
@RustanLeino
2
Dafny crashes with an exception on some quantifiers
#96 by Chris-Hawblitzel was closed Apr 5, 2017
Translation of match inside exists: Boogie name resolution error
#92 by Chris-Hawblitzel was closed Apr 4, 2017
Resolving map comprehensions and subset types
#75 by Chris-Hawblitzel was closed Feb 14, 2017
opaque, fuel, forall, triggers
#74 by Chris-Hawblitzel was closed Feb 21, 2017
@qunyanm
opaque leaked through consequence axiom
#20 by Chris-Hawblitzel was closed Sep 2, 2016
@parno
quantifiers over types that might be heap types difficulty: hard Issues that will take more than a week to fix kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) part: verifier Translation from Dafny to Boogie (translator)
#19 by Chris-Hawblitzel was closed Feb 23, 2023
1
@jtristan @RustanLeino
5
opaque and literals
#11 by Chris-Hawblitzel was closed Sep 16, 2016
@parno
1
feature request: declaring constants kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#6 by Chris-Hawblitzel was closed Nov 30, 2016
@qunyanm
3
feature request: naming function return values kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#5 by Chris-Hawblitzel was closed Jan 20, 2017
@qunyanm
1
feature request: improved char type kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#4 by Chris-Hawblitzel was closed Jan 10, 2017
@qunyanm
ProTip! Type g i on any issue or pull request to go back to the issue listing page.