Alloy cannot find an expected instance of a model when using the relational override operator. The apparent cause of this malfunction is due to a bug in Kodkod's Approximator (where it miscomputes the possible output values of the "++" operator). This small model (thanks to Greg Dennis) shows the fault:

sig A { f: lone A }
one sig X, Y extends A {}
one sig a in A {}

pred test1 {
 X.f = X
 f = f ++ (a->Y)
}

pred test2 {
 X.f = X
 f = ((f - (a->univ)) + (a->Y))
}

assert equiv {
  test1 <=> test2
}

run test1
run test2
check equiv