blob: d723cbed82150192cf9b39a42b902a7ddb943de5 (
plain)
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)
{
i := i';
call i := A(i);
assert false;
}
|