Hide instrumentation code from contracts in counterexamples

[feliperodri]

CBMC version: 5.69.1 (cbmc-5.59.0-676-gb4a4122dee)
Operating system: N/A
Exact command line resulting in the issue:
What behaviour did you expect: No instrumentation code in the counter-example.
What happened instead: Many temporary variables from function contracts instrumentation in the counter-example.

[tautschnig]

Those symbols would just need to be marked as auxiliary (or directly be created as auxiliary_symbolt, accomplishing the same).

[remi-delmas-3000]

I left these visible for debugging purposes, but now would be a good time to hide them

[feliperodri]

@tautschnig if we define them as auxiliary, can we still print them out in counterexamples on a "DEBUG" mode? There is still benefit on certain cases.

[tautschnig]

One would always get them in the JSON or XML trace; I don't think the plain-text trace ever shows them, but we could consider changing that.

[feliperodri]

If they are still visible in the JSON and XML code, then users would still see them in viewer, correct? (cc. @markrtuttle)

[tautschnig]

Was fixed in #7326.