Proposed resolution (2025-01-13, approved by CWG 2025-02-14):

Change in 11.10.3 [class.spaceship] paragraph 1 as follows:

The synthesized three-way comparison of type R (17.11.2 [cmp.categories]) of glvalues a and b of the same type is defined as follows:

• If a <=> b is usable (11.10.1 [class.compare.default]) and can be explicitly converted to R using static_cast, static_cast<R>(a <=> b).
• Otherwise, if a <=> b is usable or overload resolution for a <=> b is performed and finds at least one viable candidate, the synthesized three-way comparison is not defined.
• Otherwise, ...

The resolution accepted for issue 2539 does not actually address the example in the issue, because overload resolution is never performed for expressions involving only built-in types.