Chalice/tests/predicates/mutual-dependence.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

class Cell {
  var value: int;
  var next: Cell;
  
  predicate p { q }
  predicate q { acc(value) && acc(next) && (next != null ==> next.p) }
  
  method test()
    requires acc(this.*)
  {
    value := 1
    next := null
    fold q
    fold p
    call void()
    assert unfolding p in unfolding q in value == 1 // ERROR: should not verify
  }
  
  method void()
    requires p
    ensures p
  {}
  
}