diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc
index c6d543290f7..00d29f0d4fb 100644
--- a/regression/cbmc/Bitfields3/paths.desc
+++ b/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.
diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc
index 35db6e71ddb..96c9b4bcd7b 100644
--- a/regression/cbmc/Bitfields3/test.desc
+++ b/regression/cbmc/Bitfields3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
index 47408244d66..a190cab817e 100644
--- a/regression/cbmc/Malloc23/test.desc
+++ b/regression/cbmc/Malloc23/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc
index b0acb9b5913..f5e039ba3ed 100644
--- a/regression/cbmc/Pointer_Arithmetic11/test.desc
+++ b/regression/cbmc/Pointer_Arithmetic11/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
index e6619de477a..eb98d4f78ba 100644
--- a/regression/cbmc/Pointer_byte_extract2/test.desc
+++ b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc
index 61e6035ff74..0570ab7aba7 100644
--- a/regression/cbmc/Pointer_byte_extract9/test.desc
+++ b/regression/cbmc/Pointer_byte_extract9/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
index 998d3865da2..a584f718857 100644
--- a/regression/cbmc/Quantifiers-assignment/test.desc
+++ b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
index 9d95b7efe83..9845e70d84b 100644
--- a/regression/cbmc/byte_update3/test.desc
+++ b/regression/cbmc/byte_update3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
index 9d95b7efe83..9845e70d84b 100644
--- a/regression/cbmc/byte_update5/test.desc
+++ b/regression/cbmc/byte_update5/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc
index a821e1b3264..ff8497a9af5 100644
--- a/regression/cbmc/memory_allocation2/test.desc
+++ b/regression/cbmc/memory_allocation2/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --bounds-check
 ^EXIT=10$
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index cfbe1221019..7352faf151c 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -260,7 +260,7 @@ bool boolbvt::type_conversion(
     {
       INVARIANT(
         src_width == dest_width,
-        "source bitvector with shall equal the destination bitvector width");
+        "source bitvector width shall equal the destination bitvector width");
       dest=src;
       return false;
     }
@@ -415,24 +415,31 @@ bool boolbvt::type_conversion(
       }
       break;
 
-    default:
-      if(src_type.id()==ID_bool)
-      {
-        // bool to integer
-
+      case bvtypet::IS_BV:
         INVARIANT(
-          src_width == 1, "bitvector of type boolean shall have width one");
+          src_width == dest_width,
+          "source bitvector width shall equal the destination bitvector width");
+        dest = src;
+        return false;
 
-        for(std::size_t i=0; i<dest_width; i++)
+      default:
+        if(src_type.id() == ID_bool)
         {
-          if(i==0)
-            dest.push_back(src[0]);
-          else
-            dest.push_back(const_literal(false));
-        }
+          // bool to integer
 
-        return false;
-      }
+          INVARIANT(
+            src_width == 1, "bitvector of type boolean shall have width one");
+
+          for(std::size_t i = 0; i < dest_width; i++)
+          {
+            if(i == 0)
+              dest.push_back(src[0]);
+            else
+              dest.push_back(const_literal(false));
+          }
+
+          return false;
+        }
     }
     break;
 
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index 9dac8ffe747..d46b046d9d1 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/solvers/lowering/byte_operators.cpp
@@ -274,8 +274,11 @@ static exprt bv_to_expr(
     target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
     target_type.id() == ID_string)
   {
+    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(bitvector_expr, target_type), ns);
+      typecast_exprt::conditional_cast(bv_expr, target_type), ns);
   }
 
   if(target_type.id() == ID_struct)
@@ -371,7 +374,7 @@ static array_exprt unpack_array_vector(
       // insert offset_bytes-many nil bytes into the output array
       byte_operands.resize(
         numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
-        from_integer(0, unsignedbv_typet(8)));
+        from_integer(0, bv_typet{8}));
     }
   }
 
@@ -409,7 +412,7 @@ static array_exprt unpack_array_vector(
   const std::size_t size = byte_operands.size();
   return array_exprt(
     std::move(byte_operands),
-    array_typet(unsignedbv_typet(8), from_integer(size, size_type())));
+    array_typet{bv_typet{8}, from_integer(size, size_type())});
 }
 
 /// Extract bytes from a sequence of bitvector-typed elements.
@@ -432,7 +435,7 @@ static void process_bit_fields(
   const namespacet &ns)
 {
   const concatenation_exprt concatenation{std::move(bit_fields),
-                                          unsignedbv_typet{total_bits}};
+                                          bv_typet{total_bits}};
 
   exprt sub =
     unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns, true);
@@ -530,7 +533,7 @@ static array_exprt unpack_struct(
       const std::size_t bits_int = numeric_cast_v<std::size_t>(*component_bits);
       bit_fields->first.insert(
         little_endian ? bit_fields->first.begin() : bit_fields->first.end(),
-        typecast_exprt::conditional_cast(member, unsignedbv_typet{bits_int}));
+        typecast_exprt::conditional_cast(member, bv_typet{bits_int}));
       bit_fields->second += bits_int;
 
       member_offset_bits += *component_bits;
@@ -565,9 +568,8 @@ static array_exprt unpack_struct(
       ns);
 
   const std::size_t size = byte_operands.size();
-  return array_exprt{
-    std::move(byte_operands),
-    array_typet{unsignedbv_typet{8}, from_integer(size, size_type())}};
+  return array_exprt{std::move(byte_operands),
+                     array_typet{bv_typet{8}, from_integer(size, size_type())}};
 }
 
 /// Rewrite a complex_exprt into its individual bytes.
@@ -607,9 +609,8 @@ unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
     std::make_move_iterator(sub_imag.operands().end()));
 
   const std::size_t size = byte_operands.size();
-  return array_exprt{
-    std::move(byte_operands),
-    array_typet{unsignedbv_typet(8), from_integer(size, size_type())}};
+  return array_exprt{std::move(byte_operands),
+                     array_typet{bv_typet{8}, from_integer(size, size_type())}};
 }
 
 /// Rewrite an object into its individual bytes.
@@ -713,8 +714,7 @@ static exprt unpack_rec(
   else if(src.type().id() == ID_pointer)
   {
     return unpack_rec(
-      typecast_exprt(
-        src, unsignedbv_typet(to_pointer_type(src.type()).get_width())),
+      typecast_exprt{src, bv_typet{to_pointer_type(src.type()).get_width()}},
       little_endian,
       offset_bytes,
       max_bytes,
@@ -759,10 +759,11 @@ static exprt unpack_rec(
     for(mp_integer i=0; i<bits; i+=8)
     {
       extractbits_exprt extractbits(
-        src,
-        from_integer(i+7, index_type()),
+        typecast_exprt::conditional_cast(
+          src, bv_typet{numeric_cast_v<std::size_t>(bits)}),
+        from_integer(i + 7, index_type()),
         from_integer(i, index_type()),
-        unsignedbv_typet(8));
+        bv_typet{8});
 
       // endianness_mapt should be the point of reference for mapping out
       // endianness, but we need to work on elements here instead of
@@ -776,11 +777,11 @@ static exprt unpack_rec(
     const std::size_t size = byte_operands.size();
     return array_exprt(
       std::move(byte_operands),
-      array_typet(unsignedbv_typet(8), from_integer(size, size_type())));
+      array_typet{bv_typet{8}, from_integer(size, size_type())});
   }
 
   return array_exprt(
-    {}, array_typet(unsignedbv_typet(8), from_integer(0, size_type())));
+    {}, array_typet{bv_typet{8}, from_integer(0, size_type())});
 }
 
 /// Rewrite a byte extraction of a complex-typed result to byte extraction of
@@ -1258,7 +1259,7 @@ static exprt lower_byte_update_array_vector_non_const(
         byte_extract_exprt{extract_opcode,
                            value_as_byte_array,
                            from_integer(0, src.offset().type()),
-                           array_typet{unsignedbv_typet{8}, initial_bytes}}},
+                           array_typet{bv_typet{8}, initial_bytes}}},
       ns)};
 
   // We will update one array/vector element at a time - compute the number of
@@ -1298,7 +1299,7 @@ static exprt lower_byte_update_array_vector_non_const(
         byte_extract_exprt{extract_opcode,
                            value_as_byte_array,
                            std::move(offset_expr),
-                           array_typet{unsignedbv_typet{8}, subtype_size}}},
+                           array_typet{bv_typet{8}, subtype_size}}},
       ns);
 
     result.add_to_operands(std::move(where), std::move(element));
@@ -1318,11 +1319,11 @@ static exprt lower_byte_update_array_vector_non_const(
         src.id(),
         index_exprt{src.op(), where},
         from_integer(0, src.offset().type()),
-        byte_extract_exprt{extract_opcode,
-                           value_as_byte_array,
-                           from_integer(offset, src.offset().type()),
-                           array_typet{unsignedbv_typet{8},
-                                       from_integer(tail_size, size_type())}}},
+        byte_extract_exprt{
+          extract_opcode,
+          value_as_byte_array,
+          from_integer(offset, src.offset().type()),
+          array_typet{bv_typet{8}, from_integer(tail_size, size_type())}}},
       ns);
 
     result.add_to_operands(std::move(where), std::move(element));
@@ -1414,9 +1415,9 @@ static exprt lower_byte_update_array_vector(
       src.id(),
       index_exprt{src.op(), from_integer(i, index_type())},
       from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
-      array_exprt{std::move(update_values),
-                  array_typet{unsignedbv_typet{8},
-                              from_integer(update_size, size_type())}}};
+      array_exprt{
+        std::move(update_values),
+        array_typet{bv_typet{8}, from_integer(update_size, size_type())}}};
     elements.push_back(lower_byte_operators(bu, ns));
   }
 
@@ -1493,21 +1494,18 @@ static exprt lower_byte_update_struct(
         extract_opcode,
         src.op(),
         from_integer(0, src.offset().type()),
-        array_typet{unsignedbv_typet{8}, src_size_opt.value()}};
+        array_typet{bv_typet{8}, src_size_opt.value()}};
 
       byte_update_exprt bu = src;
       bu.op() = lower_byte_extract(byte_extract_expr, ns);
 
       return lower_byte_extract(
-        byte_extract_exprt{extract_opcode,
-                           lower_byte_update_byte_array_vector(
-                             bu,
-                             unsignedbv_typet{8},
-                             value_as_byte_array,
-                             non_const_update_bound,
-                             ns),
-                           from_integer(0, src.offset().type()),
-                           src.type()},
+        byte_extract_exprt{
+          extract_opcode,
+          lower_byte_update_byte_array_vector(
+            bu, bv_typet{8}, value_as_byte_array, non_const_update_bound, ns),
+          from_integer(0, src.offset().type()),
+          src.type()},
         ns);
     }
 
@@ -1544,11 +1542,10 @@ static exprt lower_byte_update_struct(
     const bool little_endian = src.id() == ID_byte_update_little_endian;
     if(shift != 0)
     {
-      member =
-        concatenation_exprt{typecast_exprt::conditional_cast(
-                              member, unsignedbv_typet{element_bits_int}),
-                            from_integer(0, unsignedbv_typet{shift}),
-                            unsignedbv_typet{shift + element_bits_int}};
+      member = concatenation_exprt{
+        typecast_exprt::conditional_cast(member, bv_typet{element_bits_int}),
+        from_integer(0, bv_typet{shift}),
+        bv_typet{shift + element_bits_int}};
       if(!little_endian)
         member.op0().swap(member.op1());
     }
@@ -1557,9 +1554,9 @@ static exprt lower_byte_update_struct(
       src.id(),
       std::move(member),
       offset,
-      array_exprt{std::move(update_values),
-                  array_typet{unsignedbv_typet{8},
-                              from_integer(update_size, size_type())}}};
+      array_exprt{
+        std::move(update_values),
+        array_typet{bv_typet{8}, from_integer(update_size, size_type())}}};
 
     if(shift == 0)
       elements.push_back(lower_byte_operators(bu, ns));
@@ -1569,7 +1566,7 @@ static exprt lower_byte_update_struct(
         extractbits_exprt{lower_byte_operators(bu, ns),
                           element_bits_int - 1 + (little_endian ? shift : 0),
                           (little_endian ? shift : 0),
-                          unsignedbv_typet{element_bits_int}},
+                          bv_typet{element_bits_int}},
         comp.type()));
     }
 
@@ -1701,12 +1698,12 @@ static exprt lower_byte_update(
     // build mask
     exprt mask;
     if(is_little_endian)
-      mask =
-        from_integer(power(2, update_size * 8) - 1, unsignedbv_typet{width});
+      mask = from_integer(power(2, update_size * 8) - 1, bv_typet{width});
     else
+    {
       mask = from_integer(
-        power(2, width) - power(2, width - update_size * 8),
-        unsignedbv_typet{width});
+        power(2, width) - power(2, width - update_size * 8), bv_typet{width});
+    }
 
     const typet &offset_type = src.offset().type();
     mult_exprt offset_times_eight{src.offset(), from_integer(8, offset_type)};
@@ -1722,13 +1719,13 @@ static exprt lower_byte_update(
 
     // original_bits &= ~mask
     exprt val_before =
-      typecast_exprt::conditional_cast(src.op(), unsignedbv_typet{type_bits});
+      typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
     if(width > type_bits)
     {
-      val_before = concatenation_exprt{
-        from_integer(0, unsignedbv_typet{width - type_bits}),
-        val_before,
-        unsignedbv_typet{width}};
+      val_before =
+        concatenation_exprt{from_integer(0, bv_typet{width - type_bits}),
+                            val_before,
+                            bv_typet{width}};
 
       if(!is_little_endian)
         val_before.op0().swap(val_before.op1());
@@ -1737,17 +1734,17 @@ static exprt lower_byte_update(
 
     // concatenate and zero-extend the value
     concatenation_exprt value{exprt::operandst{value_as_byte_array.operands()},
-                              unsignedbv_typet{update_size * 8}};
+                              bv_typet{update_size * 8}};
     if(is_little_endian)
       std::reverse(value.operands().begin(), value.operands().end());
 
     exprt zero_extended;
     if(width > update_size * 8)
     {
-      zero_extended = concatenation_exprt{
-        from_integer(0, unsignedbv_typet{width - update_size * 8}),
-        value,
-        unsignedbv_typet{width}};
+      zero_extended =
+        concatenation_exprt{from_integer(0, bv_typet{width - update_size * 8}),
+                            value,
+                            bv_typet{width}};
 
       if(!is_little_endian)
         zero_extended.op0().swap(zero_extended.op1());
@@ -1769,10 +1766,8 @@ static exprt lower_byte_update(
     {
       return simplify_expr(
         typecast_exprt::conditional_cast(
-          extractbits_exprt{bitor_expr,
-                            width - 1,
-                            width - type_bits,
-                            unsignedbv_typet{type_bits}},
+          extractbits_exprt{
+            bitor_expr, width - 1, width - type_bits, bv_typet{type_bits}},
           src.type()),
         ns);
     }
@@ -1840,8 +1835,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
     extract_opcode,
     src.value(),
     from_integer(0, src.offset().type()),
-    array_typet{unsignedbv_typet{8},
-                from_integer(max_update_bytes, size_type())}};
+    array_typet{bv_typet{8}, from_integer(max_update_bytes, size_type())}};
 
   const array_exprt value_as_byte_array =
     to_array_expr(lower_byte_extract(byte_extract_expr, ns));
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 7780c45ed56..410f623ea2e 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -2243,8 +2243,9 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       // this just passes through
       convert_expr(src);
     }
-    else if(src_type.id()==ID_unsignedbv ||
-            src_type.id()==ID_signedbv)
+    else if(
+      src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
+      src_type.id() == ID_bv)
     {
       // integer to pointer
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 40f417c1c81..80520b58e74 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -754,6 +754,12 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
         expr=f.to_expr();
         return false;
       }
+      else if(expr_type_id == ID_bv)
+      {
+        fixedbvt f{to_constant_expr(expr.op0())};
+        expr = from_integer(f.get_value(), expr_type);
+        return false;
+      }
     }
     else if(op_type_id==ID_floatbv)
     {
@@ -784,16 +790,47 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
         expr=fixedbv.to_expr();
         return false;
       }
+      else if(expr_type_id == ID_bv)
+      {
+        expr = from_integer(f.pack(), expr_type);
+        return false;
+      }
     }
     else if(op_type_id==ID_bv)
     {
-      if(expr_type_id==ID_unsignedbv ||
-         expr_type_id==ID_signedbv ||
-         expr_type_id==ID_floatbv)
+      if(
+        expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
+        expr_type_id == ID_c_enum || expr_type_id == ID_c_enum_tag ||
+        expr_type_id == ID_c_bit_field)
       {
         const auto width = to_bv_type(op_type).get_width();
         const auto int_value = bvrep2integer(value, width, false);
-        expr=from_integer(int_value, expr_type);
+        if(expr_type_id != ID_c_enum_tag)
+          expr = from_integer(int_value, expr_type);
+        else
+        {
+          c_enum_tag_typet tag_type = to_c_enum_tag_type(expr_type);
+          expr = from_integer(int_value, ns.follow_tag(tag_type));
+          expr.type() = tag_type;
+        }
+        return false;
+      }
+      else if(expr_type_id == ID_floatbv)
+      {
+        const auto width = to_bv_type(op_type).get_width();
+        const auto int_value = bvrep2integer(value, width, false);
+        ieee_floatt ieee_float{to_floatbv_type(expr_type)};
+        ieee_float.unpack(int_value);
+        expr = ieee_float.to_expr();
+        return false;
+      }
+      else if(expr_type_id == ID_fixedbv)
+      {
+        const auto width = to_bv_type(op_type).get_width();
+        const auto int_value = bvrep2integer(value, width, false);
+        fixedbvt fixedbv{fixedbv_spect{to_fixedbv_type(expr_type)}};
+        fixedbv.set_value(int_value);
+        expr = fixedbv.to_expr();
         return false;
       }
     }
@@ -1573,7 +1610,8 @@ optionalt<exprt> simplify_exprt::bits2expr(
   if(
     type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
     type.id() == ID_floatbv || type.id() == ID_fixedbv ||
-    type.id() == ID_c_bit_field || type.id() == ID_pointer)
+    type.id() == ID_c_bit_field || type.id() == ID_pointer ||
+    type.id() == ID_bv)
   {
     endianness_mapt map(type, little_endian, ns);
 
@@ -1769,7 +1807,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
     if(
       type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
       type.id() == ID_floatbv || type.id() == ID_fixedbv ||
-      type.id() == ID_c_bit_field)
+      type.id() == ID_c_bit_field || type.id() == ID_bv)
     {
       const auto width = to_bitvector_type(type).get_width();
 
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 8efef95340b..fbf24059f2f 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -951,7 +951,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
 
 bool simplify_exprt::simplify_shifts(exprt &expr)
 {
-  if(!is_number(expr.type()))
+  if(!is_bitvector_type(expr.type()))
     return true;
 
   if(expr.operands().size()!=2)
@@ -972,11 +972,21 @@ bool simplify_exprt::simplify_shifts(exprt &expr)
 
   auto value = numeric_cast<mp_integer>(expr.op0());
 
+  if(
+    !value.has_value() && expr.op0().type().id() == ID_bv &&
+    expr.op0().id() == ID_constant)
+  {
+    const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
+    value =
+      bvrep2integer(to_constant_expr(expr.op0()).get_value(), width, false);
+  }
+
   if(!value.has_value())
     return true;
 
-  if(expr.op0().type().id()==ID_unsignedbv ||
-     expr.op0().type().id()==ID_signedbv)
+  if(
+    expr.op0().type().id() == ID_unsignedbv ||
+    expr.op0().type().id() == ID_signedbv || expr.op0().type().id() == ID_bv)
   {
     const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
 
diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp
index 6290c725bed..0cdeb1849cd 100644
--- a/unit/solvers/lowering/byte_operators.cpp
+++ b/unit/solvers/lowering/byte_operators.cpp
@@ -150,14 +150,13 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       unsignedbv_typet(128),
       signedbv_typet(24),
       signedbv_typet(128),
-      // ieee_float_spect::single_precision().to_type(),
+      ieee_float_spect::single_precision().to_type(),
       // generates the correct value, but remains wrapped in a typecast
       // pointer_typet(u64, 64),
       vector_typet(u8, size),
       vector_typet(u64, size),
       complex_typet(s16),
-      complex_typet(u64)
-    };
+      complex_typet(u64)};
 
     simplify_exprt simp(ns);
 
@@ -301,7 +300,7 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
       unsignedbv_typet(128),
       signedbv_typet(24),
       signedbv_typet(128),
-      // ieee_float_spect::single_precision().to_type(),
+      ieee_float_spect::single_precision().to_type(),
       // generates the correct value, but remains wrapped in a typecast
       // pointer_typet(u64, 64),
       vector_typet(u8, size),