Function check_alias_vm 

pub(crate) fn check_alias_vm<'z3, 'tcx>(
    vm_state: &VmState<'z3, 'tcx>,
    checkpoint: &Checkpoint<'tcx>,
) -> VmAliasResult

Run the full alias hazard check for the VM backend.

This is the function the PropertyChecker::check_alias delegates to.