This change allows using the prophecy erasure theorem to argue that the ghost location does not change the meaning of the original program.