Use bv_typet to fix type consistency in byte-operator lowering

Previously we fixed the extracted bytes to be unsigned bitvectors, but
we should not actually imposed (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.

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.

Author: tautschnig

regression/cbmc/Array_operations1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$

regression/cbmc/Bitfields3/paths.desc

@@ -6,3 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test is marked broken-smt-backend for performance reasons only: it passes,
+but takes 5 seconds to do so.

regression/cbmc/Bitfields3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

regression/cbmc/Float-equality1/test_no_equality.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Malloc23/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/Pointer_Arithmetic11/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --little-endian
 ^EXIT=0$

regression/cbmc/Pointer_byte_extract2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=10$

regression/cbmc/Pointer_byte_extract9/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$

regression/cbmc/Quantifiers-assignment/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^\*\* Results:$

regression/cbmc/byte_update3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/byte_update5/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/memory_allocation1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/memory_allocation2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --bounds-check
 ^EXIT=10$

regression/cbmc/union12/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$

regression/cbmc/union6/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/union7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
 ^EXIT=0$

src/solvers/flattening/boolbv_typecast.cpp

@@ -415,6 +415,13 @@ bool boolbvt::type_conversion(
       }
       break;
 
+    case bvtypet::IS_BV:
+      INVARIANT(
+        src_width == dest_width,
+        "source bitvector with shall equal the destination bitvector width");
+      dest=src;
+      return false;
+
     default:
       if(src_type.id()==ID_bool)
       {