Skip to content

Commit

Permalink
Add test for issue #2748
Browse files Browse the repository at this point in the history
  • Loading branch information
MikaelMayer committed Nov 1, 2022

Verified

This commit was signed with the committer’s verified signature.
codebytere Shelley Vohr
1 parent f4bac32 commit 4dc0827
Showing 2 changed files with 13 additions and 0 deletions.
13 changes: 13 additions & 0 deletions Test/git-issues/git-issue-2748.dfy
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// RUN: %dafny_0 /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

function method f(x: int): int { 10 - x * x }

function method BindingGuardTest(): int {
var x: nat := 1;
assert true by {
if i :| 0 <= i < 10 && (f(i) == f(i+1) || f(i) == f(i+2)) {
}
}
2
}
Empty file.

0 comments on commit 4dc0827

Please sign in to comment.