Function flow_xor_violation 

fn flow_xor_violation<'z3, 'tcx>(
    vm_state: &VmState<'z3, 'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    unique: bool,
    statement_index: usize,
) -> Option<String>

Flow-sensitive shared-XOR-mutable check for a view-producing checkpoint. Walks the VM’s current locals (not a static derivation tree), grouping a live reference view as conflicting when it names the same allocation, or a sub-allocation of it (root_alloc — from_raw_parts/split_at keep a parent edge), with the opposite mutability.