Fix typing of array expressions within an C ternary ? : operator

[rod-chapman]

Fixes #9008.

Summary

For some C inputs, the SMT2 back-end emitted ill-typed SMT-LIB 2 of the form
(select <bit-vector> <index>), which conforming solvers (Bitwuzla, cvc5,
the bundled smt2_solver) reject with messages such as "select expects
array operand"; Z3 silently accepts it with a warning, which is why this
had been latent until non-Z3 solvers were used on the mlkem-native proofs.

The bug was a mismatch between smt2_convt::use_array_theory and the
encoding actually chosen by convert_expr for an array-typed if-then-else:

• convert_expr's ID_if handler emits an SMT-array ite only when at
  least one branch uses array theory; otherwise it emits a bit-vector
  ite. The asymmetric case (exactly one branch encoded as a bit-vector)
  was already handled in 769f7a2 by inserting an unflatten on the
  bit-vector branch.
• use_array_theory(if_expr), however, fell through to
  return use_datatypes || expr.id() != ID_member;, which is true
  unconditionally for ID_if.

When both branches were bit-vector-encoded — typically because they were
member accesses of a struct flattened to a bit-vector — use_array_theory
disagreed with the actual encoding, and callers (convert_index,
convert_with, flatten2bv, the array-typed define-fun path) wrapped
the bit-vector ITE in array-theory operators, producing ill-typed SMT.

This PR teaches use_array_theory the matching rule: an array-typed
if-then-else uses array theory iff at least one of its branches does.
That mirrors convert_expr in all four branch-encoding combinations
and is a companion to 769f7a2.

Regression test

regression/cbmc/issue_9008_smt_array_ite_typing exercises a conditional
pointer dereference into a struct nested in an array. Run with
--cprover-smt2, the bundled smt2_solver rejects the malformed
formula without this fix (VERIFICATION ERROR); with the fix the
assertion is reported as FAILURE as expected. The test runs as part
of the existing make -C regression/cbmc test-cprover-smt2 step in CI.

Checklist

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/ (n/a — bug fix, no user-visible behaviour change beyond producing well-typed SMT)
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed). (n/a)
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.55%. Comparing base (82ba0cc) to head (44d1337).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9012   +/-   ##
========================================
  Coverage    80.55%   80.55%           
========================================
  Files         1707     1707           
  Lines       189047   189051    +4     
  Branches        73       73           
========================================
+ Hits        152292   152296    +4     
  Misses       36755    36755           

☔ View full report in Codecov by Sentry.
📢 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.