Thanks for the report. This is now fixed in rev#92366.

the new code we have is:

	check_buffer (n: INTEGER)
			-- If there is enough space in `buffer' to read `n' bytes, do nothing.
		do
			if n + count > buffer_size then
				buffer.resize ((n + count).max (buffer.count + buffer.count // 2))
				buffer_size := buffer.count
			end
		ensure then
			buffer_adapted: n + count <= buffer_size
		end