[TS PBT] Guide relational and metamorphic properties across multiple executions #401

Closed as not planned on 2026-10-16

The project owner chose one PBT generation phase followed by USVM-only search and concrete candidate validation. The current plan is #345.

The original property can already call a function more than once and express a relational check. The current plan does not need a separate cross-execution pairing/search engine. Ordinary multi-call properties remain supported within the existing symbolic subset.

This is a scope decision, not a claim that the former acceptance was implemented. The earlier description remains in issue edit history and the pre-change audit snapshot. Reopening this extension requires a separate scope decision.