class Test {
	var x: int
	var tk: token<Test.incX>
	
	predicate V { acc(x) }
	
	method incX()
		requires V
		ensures V
	{
		unfold V
		x := x + 1
		fold V
	}
	
	method joinTk()
		requires acc(tk) && tk != null && acc(tk.joinable) && tk.joinable
		requires eval(tk.fork this.incX(), true)
		ensures V
		ensures unfolding V in x == old(x) // ERROR: old(x) is not readable (no error here, previously)
	{
		join tk
		assert V
	}

	method test()
		requires acc(x) && x == 0
		requires acc(tk)
	{
		fold V
		fork tklocal := incX()
		tk := tklocal
		call joinTk()
		unfold V
		assert x == old(x) // this verified previously (without any errors anywhere in the file)
	}
}