added a requires for the constructor that actually uses objects that need to satisfy a predicate; var declarations have to be all before statements in Boogie