Non-termination of proof on simple array copy example

[rod-chapman]

CBMC version: 6.0.0-alpha (built 12th June 2024)
Exact command line resulting in the issue: make TARGET=ctcc
What behaviour did you expect: It should work!
What happened instead:

Following issue #8303, cbmc no longer crashes but does not terminate on verification of the "ctcc" function in the latest version of code here:
https://github.com/rod-chapman/cbmc-examples/tree/main/arrays

The on-screen output ends with:

converting SSA
Runtime Convert SSA: 288.144s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 753.195s
Runtime decision procedure: 1041.34s
Running SMT2 QF_AUFBV using Z3
Runtime Solver: 2818.75s
Runtime decision procedure: 2818.75s
Running SMT2 QF_AUFBV using Z3

with very large runtimes for both the SSA conversion and subsequent Z3 runs.

This function is trivial, so I see no reason for this.

[rod-chapman]

I re-built wavefront CBMC this morning from source, and re-tried this example. The "Runtime convert SSA" phase is much better at 19 seconds (no idea why!), but Z3 is still taking forever...

[rod-chapman]

I found a problem with my code that helps. See commit
rod-chapman/cbmc-examples@b412c3f

The "assigns" contract in the loop was obviously wrong. It was

  __CPROVER_assigns(i, dst)

but it should be

__CPROVER_assigns(i, __CPROVER_object_whole(dst))

because the loop assigns to the array pointed to by dst, not the value of the dst pointer itself.

With that correction, the proof is OK in a reasonable time.

BUT... that error in the assigns clause should be reported with an easy-to-understand error message, not a giant runtime and/or non-termination of Z3, so still a problem to fix here.

[rod-chapman]

This might be the same problem as #8365

[rod-chapman]

Fixed, so close