Skip to content
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

Jump to bottom

Erroneous substitution for binding guard with case statement #2747

Closed
jtristan opened this issue Sep 15, 2022 · 0 comments · Fixed by #2759
Closed

Erroneous substitution for binding guard with case statement #2747

jtristan opened this issue Sep 15, 2022 · 0 comments · Fixed by #2759
Assignees
@jtristan
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)

Comments

@jtristan
Copy link
Contributor

jtristan commented Sep 15, 2022 •
edited
Loading

Follow up to issue #2265 with partial solution in PR #2745

function AnotherBrokenFunction(): nat {
  var y := 0;
  assert true by {
    if
    case x: bool :| true =>
      assert x;
  }
  0
}
@jtristan jtristan added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator) labels Sep 15, 2022
@jtristan jtristan self-assigned this Sep 15, 2022
@jtristan jtristan mentioned this issue Sep 19, 2022
Merged
@jtristan jtristan linked a pull request Sep 19, 2022 that will close this issue
Fix: substitution of binding guards in alternative statement correcte… #2759
Merged
jtristan added a commit that referenced this issue Sep 19, 2022
@jtristan
Fix: substitution of binding guards in alternative statement correcte… (
9c4523c 
#2759)

…d to prevent substitution of bound variable.

Fixes #2747
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jtristan jtristan

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: verifier Translation from Dafny to Boogie (translator)
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: substitution of binding guards in alternative statement correcte… dafny-lang/dafny
1 participant
@jtristan