Function check_read_memory_alias 

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