Proof/SMT explosion for simple nested loop over 2D array #8796
Description
CBMC 6.8.0 (SMT Z3 backend) produces over 3 Gigabytes of SMT2 output for a simple program that maps a function call over a 2D array of structures.
See example code here https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8796
cd 8796
make
produces q.smt2 which is 3.76GB on macOS.
Needless to say, performance of Z3 on this file is rather poor.
We also include an alternative implementation (commented out in q.c) that introduces a local copy of the struct before and after the function call. This contains the proof explostion, but introduces an unacceptable performance loss for us.