boolbv_let: pass lowered value to record_array_let_binding

[tautschnig]

convert_let computes 'lowered_value' (the let's bound expression with byte_update / byte_extract operators rewritten away by lower_byte_operators) but then dropped it on the floor and passed the un-lowered 'pair.second' to record_array_let_binding. If the let-bound array value happens to contain a byte_update, the array theory's collect_arrays will see it and trip

DATA_INVARIANT(false,
"byte_update should be removed before collect_arrays")

Fix: pass 'lowered_value' so the value handed to the array theory matches the lowering already done at the call site.

The bug was introduced by commit 14105d5 ("Connect let-bound arrays to originals in array theory"), which added the byte-operator lowering computation but forgot to thread the result through to record_array_let_binding.

Note on regression coverage: I attempted to construct a test case that triggers the DATA_INVARIANT, but could not. The set of CBMC input paths that produce an array-typed let_exprt (which is the gate at line 78 above) is currently limited to:

• SMT2 input parsed by smt2_parser.cpp — but SMT2 has no byte_update construct, so the let value cannot contain one.
• value_set_dereference.cpp — produces let-bound pointer-typed values, not array-typed; the gate above filters them out.

So the bug is currently unreachable through standard CBMC entry points, and the fix is defensive against a future code path that might funnel byte-operator-bearing array expressions into a let. The existing regression/smt2_solver/let-array/let-array.smt2 test continues to exercise the convert_let array-typed branch and passes unchanged with the fix.

• 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

Fixes a latent bug in boolbvt::convert_let where the byte-operator-lowered expression lowered_value was computed but not actually passed to record_array_let_binding, which would have caused a DATA_INVARIANT failure in collect_arrays if a let-bound array value contained a byte_update.

Changes:

• Pass lowered_value (instead of the un-lowered pair.second) to record_array_let_binding so the array theory sees an expression free of byte operators.

---

💡 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.60%. Comparing base (5453820) to head (7858db3).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9017   +/-   ##
========================================
  Coverage    80.60%   80.60%           
========================================
  Files         1711     1711           
  Lines       189466   189487   +21     
  Branches        73       73           
========================================
+ Hits        152719   152737   +18     
- Misses       36747    36750    +3     

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