Function execute_seeded 

pub fn execute_seeded(
    stmts: &[Stmt<'_>],
    interner: &Interner,
    seed: u64,
) -> Result<SymSummary, Unsupported>

Symbolically execute a nondeterministic program under a fixed seed, resolving every Select winner from a SplitMix64 mirror of the scheduler’s choice function. The result is cross-checked per-seed against run_treewalker_concurrent_seeded at the same seed, so a misaligned encoding surfaces as a disagreement — never a false proof.