- if (index != MPI_UNDEFINED)
- index_to_rank_map_.insert({index, rank});
+ if (index != MPI_UNDEFINED) {
+ if ((unsigned)index >= index_to_rank_map_.size())
+ index_to_rank_map_.resize(index + 1, MPI_UNDEFINED);
+ index_to_rank_map_[index] = rank;
+ }