Chalice/tests/predicates/test3.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
25
26
27
28
29

class Unsound
{
  var value:int;
  
  predicate inv { acc(value) }
  
  function get():int
    requires inv;
  {
    unfolding inv in value
  }
  
  method set(newval:int)
    requires inv;
    ensures inv && get()==newval;
  {
    unfold inv;
    value:=newval;
    fold inv;
  }
  
  method test()
    requires inv;
  {
    call set(3);
    call set(4);
    // at this point, Chalice used to be able to prove false
  }
}