Error byte_extract flatting of non-constant source size: byte_extract_little_endian

[mgudemann]

This file returns the following error with cbmc --cover location --unwind 3 --function "com.datastax.driver.core.VersionNumber.hashCode:()I" com/datastax/driver/core/VersionNumber.class

converting SSA
byte_extract flatting of non-constant source size: byte_extract_little_endian
  * type: pointer
      0: struct
          * tag: java::array[reference]
          * components: 
            0: 
              * type: struct
                  * incomplete_class: 1
                  * name: java::java.lang.Object
                  * tag: java.lang.Object
                  * base_name: java.lang.Object
                  * components: 
                    0: 
                      * type: string
                      * name: @class_identifier
                      * pretty_name: @class_identifier
                  * #class: 1
              * name: @java.lang.Object
            1: 
              * type: signedbv
                  * width: 32
                  * #c_type: signed_int
              * name: length
            2: 
              * type: pointer
                  0: pointer
                      * #failed_symbol: java::com.datastax.driver.core.VersionNumber.hashCode:()I::this$object
                      0: empty
              * name: data
  0: symbol
      * type: empty
      * identifier: tmp_struct_init$1!0#1
      * expression: symbol
          * type: empty
          * identifier: tmp_struct_init$1
      * L0: 0
      * L2: 1
      * #SSA_symbol: 1
  1: constant
      * type: signedbv
          * width: 64
          * #c_type: signed_long_int
      * value: 0000000000000000000000000000000000000000000000000000000000100100

a similar error appears for this method

[smowton]

Appears to have been fixed in the meantime. Not reproducible on master or test_gen.