Chalice/tests/regressions/internal-bug-4.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

class C
{
  var f: int;
  predicate valid { acc(f) }
  
  function foo1(): int
  ensures valid;
  { 1 }
  
  function foo2(): int
  ensures acc(f);
  { 1 }

  function foo3(): int
  ensures rd(f);
  { 1 }
}