[TS] Pin Yices for paired coverage remeasurement

[CaelmBleidd]

Summary

• Select the solver from the pinned coverage manifest and include it in every coverage cell identity (schema v2).
• Permit YICES in the source manifest while keeping the historical target experiment restricted to Z3.
• Reject a coverage manifest whose tool or frontend revision differs from the running build.

Validation

• Focused CallsCoverageExperimentTest and CallsExperimentTest passed with the pinned local JacoDB.
• Clean runner commit 5736a5b3664f045c0e5c15c71c832a63be0cddcc and JAR SHA-256 99ae631d34a2b938cf661f72101089c71e70b33b8f719f3131318032d7d83e38.
• The separate Yices pilot completed 13/13 cells and 4/4 universes with no tool, extraction, or replay errors. The former 165–177-second Z3 diagnostic case completed in 267 ms with 8 steps and 27/39 replayed source statements. One other pilot cell still reached the 30-second search timeout.
• The full 5,280-cell Yices campaign has not yet produced a corpus-level result. Its manifest and output directory are separate from the stopped Z3 prefix.

This PR is stacked on #416, which is stacked on #415. It changes the solver used for the new coverage campaign, not the four unknown-call policies or source corpus.