Slow down and higher memory usage with 2023-04-30 rust toolchain

[zhassan-aws]

With the 2023-04-30 rust toolchain, performance drops significantly on the BTreeSet performance regressions.

For example, with the current main (08659d3), the verification time for tests/perf/btreeset/insert_any is 1.5 seconds:

SUMMARY:
 ** 0 of 1301 failed (60 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 1.4937471s

With #2456, the verification time goes up to 141 seconds:

SUMMARY:
 ** 0 of 1306 failed (60 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 141.20958s

For tests/perf/btreeset/insert_multi, the peak memory usage with main is ~600 MB and verification time is 10 seconds:

SUMMARY:
 ** 0 of 1241 failed (46 unreachable)

 ** 2 of 2 cover properties satisfied


VERIFICATION:- SUCCESSFUL
Verification Time: 10.019767s

With #2456, CBMC runs out of memory (reaches ~26 GB after about 16 minutes).

Similar behavior is observed for tests/perf/btreeset/insert_same.

[zhassan-aws]

These are some of the CBMC statistics on the insert_any example:

[tautschnig]

It seems that the updated toolchain does even more niche optimisation, turning a further tagged union into a niche-optimised one (with the two union members using slightly different member ordering so that a pointer can be used as discriminant (when set to NULL)). diffblue/cbmc#7739 enables CBMC to cope with this case, making sure that field sensitivity can kick in to resolve a comparison against NULL at symbolic execution time.