Out of memory problem during trace printing for CaDiCaL builds on Ubuntu 18

[thomasspriggs]

A test was switched to THOROUGH in this PR - #7134
I have managed to reproduce the error seen in the associated github runner but on a local non-github machine. The machine I reproduced the issue on has 16gb of RAM and the input java for the test in question looks at least superficially straight forward. Doing some initial debugging shows that the out of memory error occurs during trace printing. Pausing the debugger as the memory is being used up leads to simplify_rec as called during build_goto_trace. Therefore this could well be an issue with infinite recursion causing the out of memory error, rather than just inadequate resources on the github runner.

This needs further investigation as I am not convinced it is solely an issue with unmaintained jbmc tests, low memory availability, or builds for older versions of Linux. This is especially concerning with regards to CaDiCaL support as I think it is only the Ubuntu 18 job which is currently running with this solver. So if want to continue supporting this solver we should setup a job with this solver in conjunction with a newer platform. Note that the Ubuntu 18 git hub actions runner is now beginning github's deprecation process - https://github.blog/changelog/2022-08-09-github-actions-the-ubuntu-18-04-actions-runner-image-is-being-deprecated-and-will-be-removed-by-12-1-22/

CBMC version: 5.65.1
Operating system: Ubuntu 18
Exact command line resulting in the issue: ctest -L CORE -R $jbmc-CORE -V -j2
or jbmc --validate-goto-model --validate--ssa-equation --validate-trace --context-include Main. Main
in /jbmc/regression/jbmc/context-include-exclude
What behaviour did you expect: Tests to pass
What happened instead: Tests failed due to out of memory during trace printing.

[kroening]

Can you dump the expression given to simplify that triggers the unbounded recursion? This should be fixed.

[thomasspriggs]

Can you dump the expression given to simplify that triggers the unbounded recursion? This should be fixed.

Ok, I have now attempted to use irept::pretty to dump the expression. However this moves the unbounded recursion into pretty instead. So there is presumably a cycle in the expression. The top level .id() is "array", but I'll need to write more custom printing code to pull out anything more useful from what now seems to be a malformed expression.

[thomasspriggs]

Unassigning as I have other work to prioritise first.

[tautschnig]

This was explained/fixed in d9b0744 (#7539): changing the solver results in models being produced that yield strings (irept representations of strings) of a size that would may exhaust the available resources. There is no real bug here, those strings are perfectly consistent with the test harness. Limiting the size of non-deterministic strings fixes the resource exhaustion.