To be clear, the optimizer doesn’t uphold the post condition. It just says “the post condition is usable to elide other checks”. But if the condition itself is

To be clear, the optimizer doesn’t uphold the post condition. It just says “the post condition is usable to elide other checks”. But if the condition itself is incorrect, the compiler will STILL elide those checks. If the compiler could prove the condition on its own it would have done so. That’s why that assert is named unchecked and is itself unsafe!