Byte-operator lowering: do not unconditionally insert bv cast

In 848e633 a cast to bv was inserted to block interpreting floatbv
type casts from taking place. It was unnecessarily inserted for all
bitvector types. While this does not result in wrong semantics, it may
block simplification for happening when we end up (via other simplifier
rules) creating a bv (and not (un)signed bv) typed constant. All of
these transformations are correct, but we may end up with an equality
over pointer-typed constants where the underlying constant is a(n)
(un)signed bv on one side, and a bv on the other side. The bit patterns
match, so the back-end will correctly solve this, but the simplifier
cannot.

Observed when studying
model-checking/kani#1978.

Author: tautschnig

src/util/lower_byte_operators.cpp

@@ -337,17 +337,22 @@ static exprt bv_to_expr(
 {
   PRECONDITION(can_cast_type<bitvector_typet>(bitvector_expr.type()));
 
-  if(
-    can_cast_type<bitvector_typet>(target_type) ||
-    target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
-    target_type.id() == ID_string)
+  if(target_type.id() == ID_floatbv)
   {
     std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
     exprt bv_expr =
       typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
     return simplify_expr(
       typecast_exprt::conditional_cast(bv_expr, target_type), ns);
   }
+  else if(
+    can_cast_type<bitvector_typet>(target_type) ||
+    target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
+    target_type.id() == ID_string)
+  {
+    return simplify_expr(
+      typecast_exprt::conditional_cast(bitvector_expr, target_type), ns);
+  }
 
   if(target_type.id() == ID_struct)
   {