path: root/Chalice/tests/regressions/workitem-10197.chalice

class Cell { var x: int } 

class Test { 
	method noop() 
		ensures old(waitlevel) == waitlevel // previously resulted in Boogie errors
	{} 
}