Connect let-bound arrays to originals in array theory

[tautschnig]

When a let expression binds a variable to an array value, the fresh symbol and the original array are disconnected in the array theory's union-find. This means Ackermann constraints and element-wise equality constraints don't propagate between them, causing spurious counterexamples in smt2_solver.

Fix: in convert_let, for array-typed bindings with unbounded array type, call record_array_equality to create an element-wise equality between the fresh variable and the bound value, and assert it as true. This connects the two representations so the array theory generates proper constraints.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• 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).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

This PR fixes missing propagation in the unbounded-array theory when arrays are introduced via let bindings, by explicitly connecting the fresh let-bound array symbol to the original array expression so array constraints (Ackermann + extensional equality) propagate correctly in smt2_solver.

Changes:

• In boolbvt::convert_let, record and assert an array equality between fresh let-bound symbols and their bound values for unbounded array types.
• Add a new smt2_solver regression test descriptor for let-bound arrays.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

File	Description
src/solvers/flattening/boolbv_let.cpp	Records/asserts array equalities for unbounded array let-bindings to connect union-find classes in array theory.
regression/smt2_solver/let-array/let-array.desc	Adds a regression descriptor intended to check the corrected let/array-theory interaction.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.46%. Comparing base (6df204e) to head (7a23bee).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8942      +/-   ##
===========================================
- Coverage    80.46%   80.46%   -0.01%     
===========================================
  Files         1704     1704              
  Lines       188665   188675      +10     
  Branches        73       73              
===========================================
+ Hits        151805   151812       +7     
- Misses       36860    36863       +3     

☔ 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.