Previously we fixed the extracted bytes to be unsigned bitvectors, but
we should not actually impose (un)signedness as we do not actually
interpret the bytes as numeric values. This fixes byte operators over
floating-point values, and makes various SMT-solver tests pass as the
SMT back-end is more strict about typing and therefore was more
frequently affected by this bug.
To make all this work it was also necessary to extend and fix the
simplifier's handling of bv_typet expressions, and also cover one more
case of type casts in the bitvector back-end.
The tests
Array_operations1/test.desc
Float-equality1/test_no_equality.desc
memory_allocation1/test.desc
union12/test.desc
union6/test.desc
union7/test.desc
continue to fail on Windows and thus cannot yet be enabled.