Merge pull request #4063 from tautschnig/byte-op-2

byte_extract lowering: ensure type consistency [blocks: #2068]

Author: tautschnig

regression/cbmc/Pointer_byte_extract3/test.desc

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

regression/cbmc/Pointer_byte_extract7/test.desc

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

regression/cbmc/equality_through_union1/test.desc

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

regression/cbmc/equality_through_union2/test.desc

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

regression/cbmc/equality_through_union3/test.desc

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

regression/cbmc/gcc_vector1/test.desc

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

regression/cbmc/trace_address_arithmetic1/test.desc

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

regression/cbmc/union11/union_list.desc

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

regression/cbmc/union8/test.desc

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

src/solvers/lowering/byte_operators.cpp

@@ -343,8 +343,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     return simplify_expr(typecast_exprt(op.front(), src.type()), ns);
   else // width_bytes>=2
   {
-    concatenation_exprt concatenation(std::move(op), src.type());
-    return simplify_expr(concatenation, ns);
+    concatenation_exprt concatenation(
+      std::move(op), bitvector_typet(subtype.id(), width_bytes * 8));
+    return simplify_expr(
+      typecast_exprt(std::move(concatenation), src.type()), ns);
   }
 }