Fix verifier reference equality across recorded upcasts

[CatarinaGamboa]

Assigning a caught IOException to an Exception local currently crashes verification with incompatible Z3 sorts. Translate mixed reference equality through an exact recorded supertype view, symmetrically for either operand order.

Preserve alias identity across native and inherited reference views with cached, on-demand solver equivalences between their equality propositions. Equality itself remains a single typed equality, so negating it for != preserves the same identity semantics. Numeric handling is unchanged; unrelated mixed reference sorts remain outside this fix.

Adds passing caught-upcast and inherited Throwable state/alias cases, failing unknown-state and already-initialized-cause cases, and solver regressions covering both equality/inequality operand orders and satisfiable distinct references.

Validation: ReferenceEqualityTest passes; both CLI fixtures produce exactly their expected outcomes. The full Java 20 CI suite passed on the final on-demand implementation; an earlier local mvn test passed 390 tests.

Fixes #377.