Skip get_literals call for unbounded arrays with zero-width elements

[tautschnig]

In convert_index, bv_width.get_width_opt(array_type) returns nullopt for unbounded arrays of zero-width elements (e.g., empty structs). The previous code used value_or(0), which passed width=0 to map.get_literals. If the identifier already existed in the boolbv_map with a non-zero literal_map size, the invariant map_entry.literal_map.size() == width would fail.

Fix: guard both get_literals calls so they are only made when the array width is known. Add regression test for this scenario.

Fixes: #8480

• 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/
• 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).
• 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.