class C { 
	method singleWarning() 
	{ assert forall i in [] :: true } // previously, quantification over the empty list resulted in Boogie errors
 
	method multipleWarnings() 
	{ assert forall i in [] :: reqIGt0(i) == i } // previously, quantification over the empty list resulted in Boogie errors
	 
	function reqIGt0(i: int): int 
		requires i >= 0 
	{ i } 
}