Test/linear/allocator.bpl


1
2
3
4
5
6
7
8
9
10

procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int);
  ensures i == i';

procedure{:entrypoint} B({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 
{
  assume i == i';
  call i := A(i);
  assert false;
}