class Test{
	var tests : seq<Test>;
	var total : int;
	
	invariant acc(tests, 100);
	invariant acc(total, 50);
	
	function at(loc : int) : Test
		requires acc(tests);
		requires loc >= 0 && loc < size();
	{
		tests[loc]
	}
	
	
	function size() : int
		requires acc(tests);
		ensures result >= 0;
		ensures result == |tests|; // previously, there was a nullpointer exception here
	{
		|tests|
	}
	
	predicate pre
	{ acc(total, 50) }
}