CBMC cannot understand Z3 generating a quantified expression in a counter-example #8679
Description
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.