The wrong result mentioned above seems to be unrelated to this bug, and has been filed as a separate BUG #747278. Thus I am closing this bug.
The wrong result mentioned above seems to be unrelated to this bug,
and has been filed as a separate BUG #747278. Thus I am closing this bug.