sqrtf appears to be non-deterministic and throwing spurious verification failures

[sree314]

CBMC version: 5.48 (but also 5.38 and 5.24)
Operating system: Ubuntu 20.04 and 18.04
Exact command line resulting in the issue: cbmc --trace sqrt.c
What behaviour did you expect: verification successful
What happened instead: verification failed and different results for sqrtf

See source code sqrt.c.txt

Also, when I add --z3 to the command line, cbmc crashes with an invariant violation report:

See report.txt

[martin-cs]

Thanks for this error report (esp. for having the stack traces enabled). I think there are two separate errors.

A. The model of sqrt
The model we use is crude but simple / lightweight, pretty accurate but non-deterministic for subnormals:

cbmc/src/ansi-c/library/math.c

Line 686 in b79bd51

/* FUNCTION: sqrtf */

The "correct" fix is to add an exprt for sqrt, get __CPROVER_sqrt to generate it, add support to the internal back-end ( similar to https://github.com/martin-cs/symfpu/blob/c3acaf62b137c36aae5eb380f1d883bfa9095f60/core/sqrt.h#L123 ) and have the SMT back-end generate fp.sqrt.

B. The crash in the SMT back-end
This is during conversion which should not happen -- looks like a bug.

[sree314]

Thanks for the reply, Martin. I was indeed encountering the issue for subnormals and I should have looked at the code :)

I'll take a stab at this sometime after Jan 24.

[tautschnig]

The crash in the SMT back-end is now addressed in #7303.