diff --git a/Test/git-issues/git-issue-2748.dfy b/Test/git-issues/git-issue-2748.dfy new file mode 100644 index 00000000000..1306aee7df9 --- /dev/null +++ b/Test/git-issues/git-issue-2748.dfy @@ -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 +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-2748.dfy.expect b/Test/git-issues/git-issue-2748.dfy.expect new file mode 100644 index 00000000000..e69de29bb2d