Unexpected verification result related to long double

[muchang]

#include <assert.h>
long double C = 2;
long double U = 1;
long double Y2 = 3;
long double Y1 = 1;
long double X, Y, Z, T, R, S;
int main ()
{
  Z = C + U + U;
  S = Z * Y2;
  Z = S - (Z + U + U);
  if (Z != 6)
    {assert(0);}
return 0; }

CBMC version:5.10
Operating system:Ubuntu 18.04
Exact command line resulting in the issue:cbmc <file.c>
What behaviour did you expect: Result in SUCCESS (proofed by compiling with gcc and executing)
What happened instead:[foo.assertion.1] assertion 0: FAILURE

[kroening]

The issue here is that compile-time rounding mode (for the initializers, and in particular for Y2) differs from rounding during the computation. This is in principle something the standard permits; in practice, this aspect is usually ignored by compiler builders.
I'll likely fix the compile-time rounding mode to the one given.