Fix byte update of struct/array elements

[tautschnig]

A key part of this is factoring out code that was almost-the-same from lower_byte_update_array_vector and lower_byte_update_struct, but actually had subtle bugs as documented in regression test included in this commit.

For consistency, do all offset calculations in bits rather than flipping back and forth between bits and bytes.

This will fix the spurious failure reported in model-checking/kani#2650.

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