CBMC version: 6.7.0, all platforms.

Recent versions of Z3 can generate quantified expressions in response to the "get-value" calls that follow a "sat" result from the prover.

CBMC cannot parse these expressions, reports an error, but fails to generate a useful trace or readable counterexample. This makes debugging failed proofs very difficult.

On the same example, switching to bitwuzla often does not help, or fails to terminate in a reasonable time.

Can we extend to CBMC to understand Z3's quantified expressions.