init {
	byte i = 0;
	do
	:: i = i+1
	od
}