Assertion index+width-1 of extractbits must be within the bitvector can fail

[tautschnig]

CSmith test with random seed 1736798452 caused:

Trying t_10.c with build 6.4.1 (50c40b3c)
**** WARNING: Use --unwinding-assertions to obtain sound verification results
CBMC version 6.4.1 (50c40b3c) 64-bit x86_64 linux
Type-checking t_10
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: flattening/boolbv_extractbits.cpp:39 function: convert_extractbits
Condition: index+width-1 of extractbits must be within the bitvector
Reason: index_as_int + bv_width - 1 < src_bv.size()
Backtrace:
cbmc() [0x4f221a]
cbmc() [0x4f2880]
cbmc() [0x449630]
cbmc() [0xa0e9d9]
cbmc() [0xa1fc50]
cbmc() [0xa0ab0a]
cbmc() [0x925369]
cbmc() [0xa09e78]
cbmc() [0xa3b7c1]
cbmc() [0xa0a8b6]
cbmc() [0x925369]
cbmc() [0xa09e78]
cbmc() [0xa0de2b]
cbmc() [0xa0dee0]
cbmc() [0x8f3ed5]
cbmc() [0x8f3b1d]
cbmc() [0x8f5812]
cbmc() [0x7ba9b7]
cbmc() [0x7bbca0]
cbmc() [0x7c4b2b]
cbmc() [0x5b6b46]
cbmc() [0x5aeb83]
cbmc() [0xb16ce3]
cbmc() [0x5a9422]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7fd86c2a6083]
cbmc() [0x40a8de]

Diagnostics:
<< EXTRA DIAGNOSTICS >>
source location:
extractbits
  * type: bv
      * width: 32
  0: typecast
      * type: bv
          * width: 28
      0: member
          * type: c_bit_field
              * #source_location:
                * file: t_10.c
                * line: 23
                * function:
                * working_directory: /home/runner/work/cbmc/cbmc/csmith.A9j
              * width: 28
              0: signedbv
                  * width: 32
                  * #c_type: signed_int
          * component_name: f0
          0: union
              * type: union_tag
                  * #source_location:
                    * file: t_10.c
                    * line: 167
                    * function:
                    * working_directory: /home/runner/work/cbmc/cbmc/csmith.A9j
                  * identifier: tag-U1
                  * #constant: 1
              * component_name: f3
              0: constant
                  * type: pointer
                      * #source_location:
                        * file: t_10.c
                        * line: 63
                        * function:
                        * working_directory: /home/runner/work/cbmc/cbmc/csmith.A9j
                      * width: 64
                      0: signedbv
                          * width: 8
                          * #typedef: int8_t
                          * #c_type: signed_char
                  * value: FFFFFFF
  1: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 0
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---