formatting.php can mess up img URLs with "x" to "times"

Hi, I am using bbPress and GD bbPress Tools on an installation.

With Tools, you can embed an image using a shortcode as such:
[img]https://example.com/wp-content/uploads/album/171/BW-600×600.png[/img]

The “x” above was being replaced by the escape code for “times” & #215; (without the space, of course).

I thought it was Tools making the conversion, because the HTML for the reply within the admin area was correct (with the “x”).

Deactivated Tools, still happening (although the image shortcode was no longer being called, of course).

Then I looked through bbPress code, then wound up in the Codex. Saw a suggestion in an article about sanitizing and escaping user data to take a look at how formatting.php works, and saw this on lines 290-294:

// 9x9 (times), but never 0x9999
if ( 1 === preg_match( '/(?<=\d)x\d/', $curl ) ) {
	// Searching for a digit is 10 times more expensive than for the x, so we avoid doing this one!
	$curl = preg_replace( '/\b(\d(?(?<=0)[\d\.,]+|[\d\.,]*))x(\d[\d\.,]*)\b/', '$1×$2', $curl );
}

That section of code is changing the “x” (meaning “by”) to the symbol “×” (meaning “times”). I just commented out those lines on this particular installation and problem solved. Then when I figure out how to update this somewhere else instead of in the core…

Suggestion: extend preg_match or add code to see if “x” is contained within a file name in the multiplication test logic.

Thank you!