I think I understand it now after several readings, but perhaps adding an example would help a lot.  ```  if (len(x) == 4) {     assert(len(y) == 5);   } else {    assert(len(y) == 5);  }  ```  In this case, both true and false branches have refined length. So the refined length after the if-statement has to be the intersection of the two.