Merge pull request #7571 from tautschnig/bugfixes/no-unconditional-cast

Byte-operator lowering: do not unconditionally insert bv cast
diffblue · Mar 6, 2023 · 6b73222 · 6b73222
2 parents e024ecb + f67691e
commit 6b73222
Showing 1 changed file with 9 additions and 4 deletions.
diff --git a/src/util/lower_byte_operators.cpp b/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)
   {