boolbv_index: handle incomplete extern array types in symbol registration

[tautschnig]

When boolbv flattens an array index expression where the array is a symbol of unbounded array_typet (e.g. an incomplete declaration like extern T arr[]), it registered that symbol with boolbv_mapt::get_literals using a width of array_width_opt.value_or(0). Passing 0 created a zero-width entry that tripped the size-equals-width invariant in get_literals when the same symbol was — or had been — registered at a non-zero width via its element-typed access path (e.g. T arr[i] returns a T-width value).

This was first surfaced by integration/linux scans of kernel sources that include <linux/ctype.h>, which declares extern const unsigned char _ctype[] — an incomplete extern array referenced by the is*() classifier macros that expand to _ctype[c]. CBMC aborted at boolbv_map.cpp:68 on every such TU.

The fix spans both back-ends, hence two commits:

• boolbv_index — Skip the registration only when the symbol is already registered at a different width. The width-0 registration itself must be preserved: it is what lets unbounded-array counterexample traces and string-refinement arrays display their element values (e.g. regression/cbmc/trace-values/unbounded_array); only the conflicting re-registration that trips the invariant is dropped. The shared guard is factored into boolbvt::register_array_symbol so the two index branches cannot drift apart.

• smt2_incremental — The incremental SMT2 back-end needs the same symbol handled once. It keyed its set of already-declared functions on the full expression irep, so the same SSA symbol reached via two sort-equivalent array-type ireps (e.g. _ctype[c] and _ctype[c + 1]) was emitted as two declare-funs, which z3 rejects (constant '_ctype#1' ... already declared). send_function_definition now deduplicates by SSA identifier, with a defensive invariant that the later expression's type is sort-equivalent to the existing declaration.

Regression test: regression/cbmc/incomplete_extern_array1/ indexes such an array at two distinct indices (forcing the symbol to be reached twice) under --bounds-check, and asserts that re-reading the same index yields the same value — so it guards against unsound flattening as well as the original invariant abort. As a CORE test it is additionally run by the cbmc-new-smt-backend CTest profile (--incremental-smt2-solver) when z3 is on PATH, which exercises the second commit.

• 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.
• 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]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Fixes a boolbv symbol-registration bug when flattening index expressions over incomplete extern T arr[] array symbols by avoiding zero-width literal-map entries, and adds a regression test reproducing the kernel _ctype[] case.

Changes:

• Skip boolbv_mapt::get_literals registration when array width is unknown during index conversion.
• Duplicate the same guard for both the byte-operator and non-byte-operator index paths.
• Add regression regression/cbmc/incomplete_extern_array1/ to prevent the invariant failure from recurring.

Reviewed changes

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

File	Description
src/solvers/flattening/boolbv_index.cpp	Avoids registering array symbols in the literal map when width is unknown, preventing zero-width invariant failures.
regression/cbmc/incomplete_extern_array1/test.desc	Adds a regression harness asserting success and absence of prior failure strings.
regression/cbmc/incomplete_extern_array1/main.c	Reproduces indexing into an incomplete extern array at multiple indices.

---

💡 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.69%. Comparing base (19dcaca) to head (bfa0251).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9055      +/-   ##
===========================================
+ Coverage    80.68%   80.69%   +0.01%     
===========================================
  Files         1714     1714              
  Lines       189519   189526       +7     
  Branches        73       73              
===========================================
+ Hits        152916   152946      +30     
+ Misses       36603    36580      -23     

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