Inconsistency with detecting infinity

[nkrusch]

This input:

y = y + 1;
y_ = y * y;
x = y_ + x;

has derivations:

   y = y + 1;  (C0)
   x  | m o o
   y  | o m o
   y_ | o o m

   y_ = y * y; (C1)
   x  | m o o
   y  | o m w
   y_ | o o o

   x = y_ + x; (C2)
   x  | m o o      x  | p o o      x  | w o o
   y  | o m o      y  | o m o      y  | o m o
   y_ | p o m      y_ | m o m      y_ | w o m

   C0; C1
   x  | m o o
   y  | o m w
   y_ | o o o

  C0; C1; C2
   x  | m o o      x  | p o o      x  | w o o
   y  | p m w      y  | w m w      y  | w m w
   y_ | o o o      y_ | o o o      y_ | o o o

Next, put the input in a while loop while( ... ) { C0; C1; C2 }

  C0; C1; C2
   x  | m o o      x  | p o o      x  | w o o
   y  | p m w      y  | w m w      y  | w m w
   y_ | o o o      y_ | o o o      y_ | o o o

          ↓               ↓               ↓
   M*              M*              M*
   x  | m o o      x  | p o o      x  | w o o
   y  | p m w      y  | p m w      y  | w m w
   y_ | o o m      y_ | o o m      y_ | o o m

With while the input fails, because rule W requires $M_{ii}^{*} = m$ and no p in matrix.

It was my assumption that delta graph reporting infinity vs. non-infinity should agree exactly with "no derivation exists" vs. "some derivation exists". However, delta graph does not report infinity here, but the analysis still correctly returns that the program is infinite, because at the end no derivation choice remains.

I am opening this issue because it bothers me these two mechanisms of DeltaGraph and Choice do not agree. By my assumption, they are supposed to arrive to the same conclusion. I briefly reviewed the FSCD paper, and my assumption of the delta graph behavior should be accurate. I suspect this is a bug.