[tautschnig]

SMT-LIB (= a b) on two arrays compares them on the entire index domain.
Only the indices 0..size-1 of a C array are constrained, though, so the
solver may pick different values for the elements out of bounds, and
__CPROVER_equal or __CPROVER_array_equal on two arrays with equal
elements fails spuriously. The propositional back-end does not have this
problem as it flattens such arrays.

For arrays of constant size up to MAX_FLATTENED_ARRAY_SIZE, the bound
the propositional back-end uses for flattening, encode the equality as
the conjunction of the equalities of the elements. Both operands are
bound once via let, so that they are not repeated per element. Larger
arrays keep the previous encoding.

This addresses the array case of #9211. Arrays that are members of a
struct encoded as an SMT-LIB datatype (with Z3 or cvc5) are compared as
part of the datatype value and are not covered by this change.

• 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.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.90%. Comparing base (266f438) to head (33e183e).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9230      +/-   ##
===========================================
- Coverage    80.91%   80.90%   -0.01%     
===========================================
  Files         1718     1718              
  Lines       190266   190290      +24     
  Branches        73       73              
===========================================
+ Hits        153952   153957       +5     
- Misses       36314    36333      +19     

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

[kroening]

There needs to be a better way here, other than enumerating up to magic constant?