Mal-formed SMT2 generated for Bitwuzla

[rod-chapman]

CBMC version: 6.1.1
Operating system: macOS
Exact command line resulting in the issue: See below
What behaviour did you expect: It works
What happened instead: Inexplicable PROOF ERROR reports

For a proof in the mlkem-aarch64 repo, we see Z3 (4.12.5) generated quantified (and non-constant) counter-examples as we have seen before. Therefore, I switched to try bitwuzla 0.5.0 instead. See attached GOTO file. Then

cbmc --flush --object-bits 10 --unwinding-assertions  --bounds-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --pointer-primitive-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --bitwuzla --outfile b.smt2 poly_compress_harness.goto

generates b.smt2 OK, but

bitwuzla b.smt2

reports

[error] b.smt2:27136:112: expected array as first argument to 'select'

Please advise. This blocks progress on mlkem-aarch64 proofs.
poly_compress_harness.goto.gz

[tautschnig]

Taking a look.

[tautschnig]

Draft fix in #8400, which appears to work with the goto binary provided in this issue. The proposed fix, however, requires more debugging as it breaks some existing regression tests.