I should add that this case with the assertion violation in `twin' is particularly problematic since, because of the call to `twin' which happens behind the scene, one cannot have an assignment. 

Interestingly, only the second assignment triggers the postcondition violation. Isn't `twin' called when assigning an expanded to a reference?