Skip to content

Commit

Permalink
add missing annotation
Browse files Browse the repository at this point in the history
  • Loading branch information
mlimbeck committed Dec 4, 2024
1 parent 880db9f commit dd43ade
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/test/resources/all/issues/silicon/0883.vpr
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
field f: Int

@moreJoins("2")
method foo(x: Ref, xs: Set[Ref])
requires forall r: Ref :: { r in xs } r in xs ==> acc(r.f)
{
Expand Down

0 comments on commit dd43ade

Please sign in to comment.