class C
{
  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 callmethod0()
    requires inv;
    ensures inv && get()==3;
  {
    call set(3);
  }
  
  method callmethod1()
  {
    call set(3); // ERROR: should fail
  }
  
  method ifc()
    requires inv;
    ensures inv && get()>old(get())
  {
    if(get()>0) { call set(get()+get()); }
    else { call set(2); }
  }
  
  method loop0() returns (r:int)
    requires inv && get()>0;
    ensures inv && r==get();
  {
    r:=0;
    while (r<unfolding inv in value)
      invariant inv && r<=get();
    { r:=r+1; }
  }
  
  method loop1() returns (r:int)
    requires inv && get()>0;
    ensures inv && r==get();
  {
    r:=0;
    while (r<get())
      invariant inv && r<=unfolding inv in value;
    { r:=r+1; }
  }
  
  method uf0()
    requires acc(value);
  {
    assert acc(value);
    fold inv;
    assert acc(value); // ERROR: should fail
  }
  
  method uf1()
    requires acc(value);
  {
    assert acc(value);
    fold inv;
    assert acc(inv);
  }
  
  method uf2()
    requires inv;
  {
    assert inv;
    unfold inv;
    assert acc(value);
  }
  
  method uf3()
    requires inv;
  {
    assert inv;
    unfold inv;
    assert acc(inv); // ERROR: should fail
  }
  
  method badframing0()
    requires get()==2;  // ERROR: should fail
  {}
  
  method badframing1()
    requires value==2; // ERROR: should fail
  {}
  
  method badframing2()
    requires acc(value) && get()==2;  // ERROR: should fail
  {}
  
  method badframing3()
    requires inv && value==2; // ERROR: should fail
  {}
}