The reason I reported this as a bug is that the compiler *does* report a
VUOT(1) error on the following:

   if attached {TEST2} Current as x and then attached {TEST3} Current as x then
   end

I couldn't immediately see a reason why this would be reported as VUOT(1)
while the submitted test case would not, since they looked very similar to me.
So I assumed this was just a bug.

Whatever you and Manu agree on is fine.  But more importantly, the behavior
of the compiler should match the ECMA Eiffel standard.  If you're not going
to report an error on the submitted test case, then the standard should
be changed (if necessary) to match what compiler writers are actually going
to implement.