[class.dtor]/12.3 causes linking to depend on run-time behavior

Example

Let us have a program Q:

struct S {
  ~S();
};
volatile int x=0;
int main() {
  S s;
  while(true)
    x = 1;
}

Is the destructor S::~S is odr-used in Q? I guess we want it to be the case. Can we prove that from the wording? Let us try this line of reasoning:

Proof fails

[basic.def.odr]/8

A destructor for a class is odr-used if it is potentially invoked

[class.dtor]/12

A destructor is potentially invoked if it is invoked or as specified in 7.6.2.4, 9.3.1, 10.9.2,
and 13.1.

[class.dtor]/12 (again)

A destructor is invoked implicitly [...] for a constructed object with automatic storage duration (6.6.4.3) > when the block in which an object is created exits.

From the source code of Q:

The block in which a variable of a class type S is declared, exits.

But the block does not exit. So the argument fails.

Discussion

Sure, the block ends - at some position in the source code. But it does not exit. The term "Exit of a block" refers to an execution event, not to a place in source code. Compare with [stmt.jump]/8:

On exit from a scope (however accomplished), objects with automatic storage duration (6.6.4.3)
that have been constructed in that scope are destroyed in the reverse order of their construction.

Another argument is that the standard does not say

A destructor is invoked implicitly [...] where the block in which an object is created exits.

or

A destructor is invoked implicitly [...] if the block in which an object is created exits.

but

A destructor is invoked implicitly [...] when the block in which an object is created exits.

In other words, it says:

At the time when the program is running and the block exits, the destructor is implicitly invoked.

It does not say:

At the place of the source code where the block ends, the destructor is implicitly invoked.

But how can a link-time property (odr-use) depend on an execution event?

Other

Based on this discussion. I came across this problem when working on a formal semantics of C++.

Start by reading [basic.def.odr]/8 and [class.dtor]/12 in the draft, then compare the cited wording with [stmt.jump]/8 and the linked discussion. Determine whether the example's destructor is odr-used despite the infinite loop, and clarify the standard wording if the current reasoning cannot establish that result.