range over maps requires with clause unconditionally

[gottschali]

For range loops over maps, one has to add with visited even if visited is not used.
Otherwise, we get an error "Loop invariant might not be established".

// @ requires acc(m)
func mapRange(m map[int]int) {
	//@ invariant acc(m)
	for k, v := range m {}
}

This is inconsistent with slices where it is not mandatory.

// @ requires acc(s)
func sliceRange(s []int) {
	//@ invariant acc(s)
	for i, e := range s {}
}