Re: [GHC] #16003: Average and maximum residency numbers in nofib broken