SMT2 back-end emits ill-typed terms for flattened aggregates

[fcasal]

Summary

Two aggregate-expression paths can produce invalid SMT-LIB:

• A struct with two leading zero-width fields and one non-zero-width field is
  emitted as unary concat. This bug is directly reachable from ordinary C;
  a complete reproducer is below.
• An array-valued let can be treated as an SMT array even when its body or
  bound value is emitted as a bit-vector. This is a valid internal expression,
  but no C front-end reproducer is currently known.

The relevant code is the struct concatenation loop, its duplicate in
datatype flattening, the let emitter, and the array encoding classifier.
The array case is the same class of sort mismatch as #9008, but for let
rather than if expressions.

C reproducer: zero-width struct fields

#include <assert.h>

struct S
{
  unsigned char : 0;
  unsigned char : 0;
  unsigned char value;
};

union U
{
  struct S structure;
  unsigned char value;
};

int main(int argc, char **argv)
{
  (void)argv;
  unsigned char value = (unsigned char)argc;

  union U object = {.structure = {.value = value}};
  assert(object.value == value);
}

Save this as main.c and run an affected CBMC build with Bitwuzla support:

cbmc --bitwuzla main.c

The assertion is valid, but CBMC reports the property as ERROR and ends with
VERIFICATION ERROR. To see the parser error directly, save and check the
generated formula:

cbmc --smt2 --outfile formula.smt2 main.c
bitwuzla formula.smt2

Bitwuzla 0.9.1 reports:

expected at least 2 arguments to 'concat', got 1

In CBMC's layout, the unsigned char fields make this a one-byte struct whose
only non-zero-width component is value. The union initialization forces it
into a bit-vector. Non-datatype backends use the struct encoder; datatype
backends use the duplicate flattening loop. Before the fix, both paths produce:

(concat value)

Z3 accepts unary concat as an extension, so it does not expose the error.

Internal reproducer: array-valued let

For an array-valued let whose body is a flattened array member, indexing the
result produces:

(select
  (let ((scalar (_ bv0 8))) ((_ extract 15 0) structure))
  (_ bv0 8))

Bitwuzla rejects it with:

expected array as first argument to 'select'

The bundled CPROVER SMT2 parser reports select expects array operand for this
form. Bitwuzla reports the error above. C-generated let expressions are
normally lifted before solving; the retained cases tested so far reconstruct
their arrays with array theory and do not trigger this mismatch.

Affected back-ends

The struct-construction and array-let cases use the non-datatype encoding:
generic SMT2 output, Bitwuzla, Boolector, CPROVER SMT2, MathSAT, and Yices.
Z3 and CVC5 normally avoid those paths, but the duplicate concat bug is also
reachable when one of their datatype structs is explicitly flattened to a
bit-vector.

The linked source revision is a777c7b2. The C reproducer and the internal
expressions were checked with Bitwuzla 0.9.1.

Proposed fix

Build struct concatenations from the non-zero-width components, and emit no
concat when only one remains.

For array-valued let expressions, derive the encoding from the emitted body.
Inline bindings whose array values are already flattened so that an SMT array
variable is never bound to a bit-vector value.