Crash when passing cbmc file with very large expressions in assumptions

[martinlester]

CBMC version: 5.83.0 (cbmc-5.83.0) 64-bit x86_64 linux
Operating system: Debian 12
Exact command line resulting in the issue: cbmc nonogram-crash.c
What behaviour did you expect: CBMC returns verification succeeded/failed
What happened instead: CBMC crashes at some point before passing to SAT solver

It takes about a minute for CBMC to crash with this file. It has some very large assumptions that encode a constraint problem. I can work around this by splitting them up into smaller assumptions, but all the same, I think the crash is a bug.

$ cbmc nonogram-crash.c 
CBMC version 5.83.0 (cbmc-5.83.0) 64-bit x86_64 linux
Parsing nonogram-crash.c
Converting
Type-checking nonogram-crash
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Segmentation fault

nonogram-crash.c.gz

[tautschnig]

Thank you for this report and the example. We really need to refactor various places in our code base that recursively traverse expressions and use exprt::visit_pre, exprt::visit_post, or depth_iteratort instead.