v0.8.5 — havoc'd guards and faster whole-project verify

Three fixes born from one bug report — a comparator refuted with an impossible result = 2 and an irrelevant aliasing note.

Havoc'd ternary guards. When a condition doesn't translate (optional chains, string methods, unknown calls), it becomes a free boolean instead of dropping the whole body equation. Branch-structure properties now prove without the solver understanding the guard:

ensures(output() === -1 || output() === 0 || output() === 1)   // ✓ PROVED
const lastNameA = a?.lastName?.toLowerCase() || "";            // opaque guard — fine
if (lastNameA < lastNameB) return -1;
...

Sound overapproximation: a refutation under a havoc'd guard may pick an infeasible branch — strictly better than the free result that produced impossible counterexamples.

Faster whole-project verify. The orchestrator pre-filters before sharding: only files carrying contracts/schema parses or mentioning a registered function reach the solver. On a 2k-file application: 2121 files → 586 relevant, 7m37s → 3m32s.

Counterexample de-noising. Ref-array aliasing notes (same object as) and raw ref maps are suppressed when the query never reads array elements — slot identities there are arbitrary model choices, not information.

~325 core tests.