goto-instrument -dfcc spurious warnings

[rod-chapman]

In the proofs of mlkem-native and mldsa-native, goto-instrument -dfcc always produces the following 5 warnings on stderr every time. These are meaningless and clutter CI logs. Can they be removed please?

For example:

$ goto-instrument -dfcc harness c5.goto c6.goto 1>stdout.txt

file <builtin-library-malloc> line 6: symbol '__CPROVER_malloc_is_new_array' already has an initial value

symbol '__CPROVER_alloca_object' already has an initial value

symbol '__CPROVER_new_object' already has an initial value

file <builtin-library-free> line 11: symbol '__CPROVER_malloc_is_new_array' already has an initial value

generate function bodies: No function name matched regex