SMT and proof time explosion looping over array(s)

[rod-chapman]

Another test case where proof blows up. This time, even the CBMC built with the branch from PR#8705 still fails.

Hopefully a refinement of work on that branch will fix this also.

Small test case will be linked in a comment below.

[rod-chapman]

Test case: https://github.com/rod-chapman/cbmc-examples/tree/main/issues/8821

cd 8821
make

produces q.smt2 which is 22.6 Megabytes. Z3 does not return a useful result in any reasonable time.

If you change to the "workaround" version in the sources, CBMC produces a 2.3Mb SMT file, which proves "unsat" in about 15 seconds on my laptop.

[tautschnig]

Thank you for this compact example. I can confirm that I can reproduce the problem. Will debug.

[rod-chapman]

This test case still fails after PR#8705 has been merged.

[tautschnig]

This might not actually require a fix in CBMC: please remove --no-array-field-sensitivity to enable CBMC to propagate the necessary information to make this test work quickly (8 seconds for me).