[BitBucket user: Ben Bloom]
[BitBucket date: 2017-10-26.11:53:40]

I found that there was an additional difference in the file, namely, there were two extra bytes at its tail. Removing these bytes seems to resolve the issue. 
First, let me apologize for the false alarm. And then, I think the issue may be closed as "not a bug".
Thanks!