diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index 02986e1442a..1b328757845 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -337,10 +337,7 @@ static exprt bv_to_expr( { PRECONDITION(can_cast_type(bitvector_expr.type())); - if( - can_cast_type(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 = @@ -348,6 +345,14 @@ static exprt bv_to_expr( return simplify_expr( typecast_exprt::conditional_cast(bv_expr, target_type), ns); } + else if( + can_cast_type(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) {