In the documentation for ghost mappings, there are multiple instances of =
instead of ==
. Please update this.
For example
havoc myGhostMapping assuming forall k. k = j ?
myGhostMapping@new[k] = x :
myGhostMapping@new[k] = myGhostMapping@old[k];