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
2 Open 26 Closed
2 Open 26 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

Incorrect C# compilation of discriminators with underscores kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime
#1607 by jaylorch was closed Nov 26, 2021
1
@fabiomadge
Strengthening drop/update commutativity axiom kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#1423 by jaylorch was closed Apr 29, 2022
1
1
Multiplicative associativity prelude axiom can cause matching loop
#1248 by jaylorch was closed Jun 11, 2021
1
Regression in set reasoning kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
#1223 opened May 12, 2021 by jaylorch
1
Subtracting from map causes translator crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#1184 by jaylorch was closed Apr 16, 2021
1
Visual Studio build always runs Coco
#1123 by jaylorch was closed Feb 22, 2021
1
2
stdin.dfy doesn't work kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#1109 by jaylorch was closed Mar 25, 2021
2
1
Repeating destructor name causes long verification times area: performance Performance issues part: verifier Translation from Dafny to Boogie (translator)
#655 opened Jun 6, 2020 by jaylorch
1
Dafny ignores module specifier, giving specious error kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#235 by jaylorch was closed Jun 17, 2019
rprint doesn't preserve important parentheses
#228 by jaylorch was closed Feb 21, 2019
2
Dafny crashes when quantifier appears in implicit trigger
#215 by jaylorch was closed Apr 5, 2019
1
Dafny crashes on update to instance of generic type
#214 by jaylorch was closed Oct 31, 2018
2
Can prove false using inconsistent definition of map cardinality
#135 by jaylorch was closed Aug 23, 2017
2
Extensionality axioms for datatypes kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
#133 by jaylorch was closed Mar 13, 2019
4
Dafny crashes on non-existent type
#99 by jaylorch was closed Apr 25, 2017
Dafny hits stack overflow exception
#98 by jaylorch was closed Apr 17, 2017
3
Dafny crashes when using datatype constructor from another module
#89 by jaylorch was closed Jun 20, 2017
3
Revealing an opaque function doesn't work if it calls another opaque function
#56 by jaylorch was closed Jul 1, 2017
2
Hiding a type with a restrictive export set doesn't prevent a type ambiguity error
#50 by jaylorch was closed Oct 26, 2016
@qunyanm
Dafny crashes when an exported revealed function depends on a private type
#49 by jaylorch was closed Oct 27, 2016
@qunyanm
Using forall in an included file causes crash
#48 by jaylorch was closed Oct 21, 2016
@qunyanm
Dafny crashes when including module
#47 by jaylorch was closed Oct 21, 2016
@qunyanm
Dafny tries to re-verify lemma from abstract module when refined in another file kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
#46 by jaylorch was closed Oct 20, 2016
1
@qunyanm
Dafny can't see fact about subset type in calc
#41 by jaylorch was closed Oct 7, 2016
@qunyanm
6
Dafny extension verification crashes when tuple#2 is used.
#38 by jaylorch was closed Oct 6, 2016
@qunyanm
ProTip! Mix and match filters to narrow down what you’re looking for.