Multiplication of complex number is modelled incorrectly

[andreast271]

CBMC version: 6.0.2
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc complex.c
What behaviour did you expect: assertion "right" succeeds, assertion "wrong" fails
What happened instead: assertion "right" fails, assertion "wrong" succeeds

Here is the code of complex.c:

#include <complex.h>

int main() {
  char choice;
  float re = choice ? 1.3f : 2.1f; // a non-constant well-behaved float
  float complex z1 = I + re;
  float complex z2 = z1 * z1;
  float complex expected = 2*I*re + re*re - 1; // (a+i)^2 = 2ai + a^2 - 1 
  float complex actual = re*re + I; // (a1 + b1*i)*(a2 + b2*i) = (a1*a2 + b1*b2*i)
  __CPROVER_assert(z2 == expected, "right");
  __CPROVER_assert(z2 == actual, "wrong");
  return 0;
}

CBMC behaves as if complex multiplication was done separately for the real and the imaginary part, like complex addition. I.e. (a*b).real = a.real * b.real and (a*b).img = a.img * b.img . That is not how this works.

[tautschnig]

Thank you for the report and helpful test. #8376 will eventually fix this, but still requires further work as not only the back-end was broken, but also remove_complex needs fixing.