Skip to content

Commit 3d95d76

Browse files
authored
Testcase for Silicon issue 883 (#821)
1 parent 08c001b commit 3d95d76

1 file changed

Lines changed: 16 additions & 0 deletions

File tree

  • src/test/resources/all/issues/silicon
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
field f: Int
2+
3+
@moreJoins("2")
4+
method foo(x: Ref, xs: Set[Ref])
5+
requires forall r: Ref :: { r in xs } r in xs ==> acc(r.f)
6+
{
7+
var b: Bool
8+
inhale acc(x.f, 1/2)
9+
if (b) {
10+
inhale acc(x.f, 1/2)
11+
} else {
12+
inhale acc(x.f, 1/2)
13+
}
14+
15+
assert acc(x.f)
16+
}

0 commit comments

Comments
 (0)