Fix ill-typed SMT2 for flattened aggregate expressions

[fcasal]

Fixes #9146.

Problem

The SMT2 aggregate encoding could emit two invalid terms:

• (concat value) for a struct with several zero-width fields and only one
  non-zero-width field
• (select <bit-vector> index) for an array-valued let whose body or bound
  value is a flattened struct member

Strict SMT-LIB parsers reject these terms instead of checking the program.
The unary concat case is reachable from C using structs with unnamed
zero-width unsigned char bit-fields. No C producer is currently known for the
array-valued let case; it is covered as an internal converter invariant.

Change

Struct conversion now collects the non-zero-width component indices first and
adds exactly one binary concat per additional component. The datatype
flattening path uses the same helper.

Array-valued let expressions now follow the encoding of their emitted body.
Bindings whose array values use the flattened bit-vector encoding are inlined;
other bindings remain in the SMT let.

Tests

unit/solvers/smt2/smt2_conv.cpp now checks:

• a struct with two empty fields and one 8-bit field is emitted directly,
  without unary concat
• mixed empty and non-empty struct fields preserve their bit-vector order
• flattening the equivalent datatype struct to a bit-vector also avoids unary
  concat
• indexing an array-valued let uses bit-vector extraction when its body is a
  flattened struct member
• flattened array bindings are inlined
• unrelated scalar bindings remain in the emitted let
• bindings that genuinely use array theory remain in the emitted let

regression/cbmc/smt2_zero_width_struct_concat provides a C reproducer. It
stores the struct in a union, exercising both non-datatype struct conversion
and datatype-to-bit-vector flattening.

The focused failure cases emit unary concat or apply select to a bit-vector
on develop. The other sections guard component order and ensure array-theory
bindings are not unnecessarily inlined.

Verification

$ cmake --build build --target unit -j4
$ ./build/bin/unit 'smt2_convt does not emit unary concat'
All tests passed (10 assertions in 1 test case)

$ ./build/bin/unit 'smt2_convt array-valued let uses the emitted array encoding'
All tests passed (14 assertions in 1 test case)

$ ./build/bin/unit '[core][solvers][smt2]'
All tests passed (213 assertions in 40 test cases)

The malformed examples from the issue were also checked with Bitwuzla 0.9.1.
It rejects both original forms and accepts the corrected formulas. The bundled
CPROVER SMT2 parser rejects the array sort mismatch and accepts both corrected
forms.

The C regression passes with the default SMT2 configuration, CPROVER SMT2,
Bitwuzla, and Z3. With the old encoder, Bitwuzla reports the property as ERROR
and exits with VERIFICATION ERROR.

[codecov]

Codecov Report

❌ Patch coverage is 99.37888% with 1 line in your changes missing coverage. Please review.
✅ Project coverage is 81.40%. Comparing base (a777c7b) to head (a695bd5).

Files with missing lines	Patch %	Lines
src/solvers/smt2/smt2_conv.cpp	98.27%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9147      +/-   ##
===========================================
+ Coverage    80.83%   81.40%   +0.57%     
===========================================
  Files         1715     1715              
  Lines       189989   211603   +21614     
  Branches        73       73              
===========================================
+ Hits        153576   172264   +18688     
- Misses       36413    39339    +2926     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.