Thanks for reporting this. This is a known issue with the backend C compiler which performs comparison with a higher precision than the value stored thus causing the post-condition to fail.