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
  }
}