Added one more post-condition to fseek. And surprise surprise, it's not valid