diff --git a/src/solvers/Makefile b/src/solvers/Makefile
index fdeed7e705c..78831a103a8 100644
--- a/src/solvers/Makefile
+++ b/src/solvers/Makefile
@@ -140,7 +140,6 @@ SRC = $(BOOLEFORCE_SRC) \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \
       floatbv/float_approximation.cpp \
-      lowering/byte_operators.cpp \
       lowering/functions.cpp \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index c2871932357..01cb688063f 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -14,8 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 bvt map_bv(const endianness_mapt &map, const bvt &src)
 {
   PRECONDITION(map.number_of_bits() == src.size());
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 9216e17c8ad..3d94761b5a8 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/byte_operators.h>
 #include <util/invariant.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
   // if we update (from) an unbounded array, lower the expression as the array
diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp
index a7e6d2b98c7..8e604fe9ac1 100644
--- a/src/solvers/flattening/boolbv_equality.cpp
+++ b/src/solvers/flattening/boolbv_equality.cpp
@@ -10,8 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 #include <util/std_expr.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 #include "boolbv.h"
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index 01884ea3503..f2b0ac59fef 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 bvt boolbvt::convert_index(const index_exprt &expr)
 {
   const exprt &array=expr.array();
diff --git a/src/solvers/lowering/expr_lowering.h b/src/solvers/lowering/expr_lowering.h
deleted file mode 100644
index bb0bde32a08..00000000000
--- a/src/solvers/lowering/expr_lowering.h
+++ /dev/null
@@ -1,44 +0,0 @@
-/*******************************************************************\
-
-Module: Lower expressions to arithmetic and logic expressions
-
-Author: Michael Tautschnig
-
-\*******************************************************************/
-
-#ifndef CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
-#define CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
-
-#include <util/expr.h>
-
-class byte_extract_exprt;
-class byte_update_exprt;
-class namespacet;
-
-/// Rewrite a byte extract expression to more fundamental operations.
-/// \param src: Byte extract expression
-/// \param ns: Namespace
-/// \return Semantically equivalent expression such that the top-level
-///   expression no longer is a \ref byte_extract_exprt or
-///   \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
-///   byte operators from any operands of \p src.
-exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
-
-/// Rewrite a byte update expression to more fundamental operations.
-/// \param src: Byte update expression
-/// \param ns: Namespace
-/// \return Semantically equivalent expression such that the top-level
-///   expression no longer is a \ref byte_extract_exprt or
-///   \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
-///   byte operators from any operands of \p src.
-exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
-
-/// Rewrite an expression possibly containing byte-extract or -update
-/// expressions to more fundamental operations.
-/// \param src: Input expression
-/// \param ns: Namespace
-/// \return Semantically equivalent expression that does not contain any \ref
-///   byte_extract_exprt or \ref byte_update_exprt.
-exprt lower_byte_operators(const exprt &src, const namespacet &ns);
-
-#endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 9541c2d6c8e..1c3d338e972 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -38,7 +38,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
 #include <solvers/floatbv/float_bv.h>
-#include <solvers/lowering/expr_lowering.h>
 #include <solvers/prop/literal_expr.h>
 
 #include "smt2_tokenizer.h"
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index f1d0d2e52c4..3170c7b45ee 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -3,6 +3,7 @@
 #include "smt2_incremental_decision_procedure.h"
 
 #include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/expr.h>
 #include <util/namespace.h>
 #include <util/nodiscard.h>
@@ -11,7 +12,6 @@
 #include <util/string_utils.h>
 #include <util/symbol.h>
 
-#include <solvers/lowering/expr_lowering.h>
 #include <solvers/smt2_incremental/ast/smt_commands.h>
 #include <solvers/smt2_incremental/ast/smt_responses.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
diff --git a/src/util/Makefile b/src/util/Makefile
index d08eb263960..30452e2e302 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -46,6 +46,7 @@ SRC = arith_tools.cpp \
       json_stream.cpp \
       lispexpr.cpp \
       lispirep.cpp \
+      lower_byte_operators.cpp \
       mathematical_expr.cpp \
       mathematical_types.cpp \
       memory_info.cpp \
diff --git a/src/util/byte_operators.h b/src/util/byte_operators.h
index f8dc2289fab..1476234f4cd 100644
--- a/src/util/byte_operators.h
+++ b/src/util/byte_operators.h
@@ -166,4 +166,30 @@ make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
 /// update expression.
 bool has_byte_operator(const exprt &src);
 
+/// Rewrite a byte extract expression to more fundamental operations.
+/// \param src: Byte extract expression
+/// \param ns: Namespace
+/// \return Semantically equivalent expression such that the top-level
+///   expression no longer is a \ref byte_extract_exprt or
+///   \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
+///   byte operators from any operands of \p src.
+exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
+
+/// Rewrite a byte update expression to more fundamental operations.
+/// \param src: Byte update expression
+/// \param ns: Namespace
+/// \return Semantically equivalent expression such that the top-level
+///   expression no longer is a \ref byte_extract_exprt or
+///   \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
+///   byte operators from any operands of \p src.
+exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
+
+/// Rewrite an expression possibly containing byte-extract or -update
+/// expressions to more fundamental operations.
+/// \param src: Input expression
+/// \param ns: Namespace
+/// \return Semantically equivalent expression that does not contain any \ref
+///   byte_extract_exprt or \ref byte_update_exprt.
+exprt lower_byte_operators(const exprt &src, const namespacet &ns);
+
 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/util/lower_byte_operators.cpp
similarity index 94%
rename from src/solvers/lowering/byte_operators.cpp
rename to src/util/lower_byte_operators.cpp
index cc4f2278ad6..500472e62ce 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/util/lower_byte_operators.cpp
@@ -6,19 +6,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include <util/arith_tools.h>
-#include <util/bitvector_expr.h>
-#include <util/byte_operators.h>
-#include <util/c_types.h>
-#include <util/endianness_map.h>
-#include <util/expr_util.h>
-#include <util/namespace.h>
-#include <util/narrow.h>
-#include <util/pointer_offset_size.h>
-#include <util/simplify_expr.h>
-#include <util/string_constant.h>
-
-#include "expr_lowering.h"
+#include "arith_tools.h"
+#include "bitvector_expr.h"
+#include "byte_operators.h"
+#include "c_types.h"
+#include "endianness_map.h"
+#include "expr_util.h"
+#include "namespace.h"
+#include "narrow.h"
+#include "pointer_offset_size.h"
+#include "simplify_expr.h"
+#include "string_constant.h"
 
 #include <algorithm>
 
@@ -147,9 +145,10 @@ static union_exprt bv_to_union_expr(
 
   if(component_bits == 0)
   {
-    return union_exprt{components.front().get_name(),
-                       constant_exprt{irep_idt{}, components.front().type()},
-                       union_type};
+    return union_exprt{
+      components.front().get_name(),
+      constant_exprt{irep_idt{}, components.front().type()},
+      union_type};
   }
 
   const auto bounds = map_bounds(endianness_map, 0, component_bits - 1);
@@ -475,9 +474,10 @@ static exprt unpack_array_vector_no_known_bounds(
       std::to_string(array_comprehension_index_counter),
     c_index_type()};
 
-  index_exprt element{src,
-                      div_exprt{array_comprehension_index,
-                                from_integer(el_bytes, c_index_type())}};
+  index_exprt element{
+    src,
+    div_exprt{
+      array_comprehension_index, from_integer(el_bytes, c_index_type())}};
 
   exprt sub =
     unpack_rec(element, little_endian, {}, {}, bits_per_byte, ns, false);
@@ -643,8 +643,8 @@ static void process_bit_fields(
   const std::size_t bits_per_byte,
   const namespacet &ns)
 {
-  const concatenation_exprt concatenation{std::move(bit_fields),
-                                          bv_typet{total_bits}};
+  const concatenation_exprt concatenation{
+    std::move(bit_fields), bv_typet{total_bits}};
 
   exprt sub = unpack_rec(
     concatenation,
@@ -869,9 +869,9 @@ static exprt unpack_rec(
   const namespacet &ns,
   bool unpack_byte_array)
 {
-  if(src.type().id()==ID_array)
+  if(src.type().id() == ID_array)
   {
-    const array_typet &array_type=to_array_type(src.type());
+    const array_typet &array_type = to_array_type(src.type());
     const typet &subtype = array_type.element_type();
 
     auto element_bits = pointer_offset_bits(subtype, ns);
@@ -986,7 +986,7 @@ static exprt unpack_rec(
       ns,
       unpack_byte_array);
   }
-  else if(src.type().id()!=ID_empty)
+  else if(src.type().id() != ID_empty)
   {
     // a basic type; we turn that into extractbits while considering
     // endianness
@@ -1120,9 +1120,10 @@ static exprt lower_byte_extract_array_vector(
   body.type() = subtype;
   body.offset() = std::move(new_offset);
 
-  return array_comprehension_exprt{std::move(array_comprehension_index),
-                                   lower_byte_extract(body, ns),
-                                   array_type};
+  return array_comprehension_exprt{
+    std::move(array_comprehension_index),
+    lower_byte_extract(body, ns),
+    array_type};
 }
 
 /// Rewrite a byte extraction of a complex-typed result to byte extraction of
@@ -1273,10 +1274,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   }
   else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
   {
-    const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
-    const struct_typet::componentst &components=struct_type.components();
+    const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
+    const struct_typet::componentst &components = struct_type.components();
 
-    bool failed=false;
+    bool failed = false;
     struct_exprt s({}, src.type());
 
     for(const auto &comp : components)
@@ -1288,7 +1289,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
         !component_bits.has_value() || *component_bits == 0 ||
         *component_bits % src.get_bits_per_byte() != 0)
       {
-        failed=true;
+        failed = true;
         break;
       }
 
@@ -1307,8 +1308,8 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
           member_offset_opt.value(), unpacked.offset().type()));
 
       byte_extract_exprt tmp(unpacked);
-      tmp.type()=comp.type();
-      tmp.offset()=new_offset;
+      tmp.type() = comp.type();
+      tmp.offset() = new_offset;
 
       s.add_to_operands(lower_byte_extract(tmp, ns));
     }
@@ -1334,8 +1335,8 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     }
   }
 
-  const exprt &root=unpacked.op();
-  const exprt &offset=unpacked.offset();
+  const exprt &root = unpacked.op();
+  const exprt &offset = unpacked.offset();
 
   optionalt<typet> subtype;
   if(root.type().id() == ID_vector)
@@ -1369,11 +1370,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   exprt::operandst op;
   op.reserve(width_bytes);
 
-  for(std::size_t i=0; i<width_bytes; i++)
+  for(std::size_t i = 0; i < width_bytes; i++)
   {
     // the most significant byte comes first in the concatenation!
-    std::size_t offset_int=
-      little_endian?(width_bytes-i-1):i;
+    std::size_t offset_int = little_endian ? (width_bytes - i - 1) : i;
 
     plus_exprt offset_i(from_integer(offset_int, offset.type()), offset);
     simplify(offset_i, ns);
@@ -1394,7 +1394,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     }
   }
 
-  if(width_bytes==1)
+  if(width_bytes == 1)
   {
     return simplify_expr(
       typecast_exprt::conditional_cast(op.front(), src.type()), ns);
@@ -1450,9 +1450,10 @@ static exprt lower_byte_update_byte_array_vector_non_const(
     typecast_exprt::conditional_cast(
       array_comprehension_index, non_const_update_bound.type()),
     ID_ge,
-    plus_exprt{typecast_exprt::conditional_cast(
-                 src.offset(), non_const_update_bound.type()),
-               non_const_update_bound}};
+    plus_exprt{
+      typecast_exprt::conditional_cast(
+        src.offset(), non_const_update_bound.type()),
+      non_const_update_bound}};
 
   if_exprt array_comprehension_body{
     or_exprt{std::move(lower_bound), std::move(upper_bound)},
@@ -1460,15 +1461,17 @@ static exprt lower_byte_update_byte_array_vector_non_const(
     typecast_exprt::conditional_cast(
       index_exprt{
         value_as_byte_array,
-        minus_exprt{array_comprehension_index,
-                    typecast_exprt::conditional_cast(
-                      src.offset(), array_comprehension_index.type())}},
+        minus_exprt{
+          array_comprehension_index,
+          typecast_exprt::conditional_cast(
+            src.offset(), array_comprehension_index.type())}},
       subtype)};
 
   return simplify_expr(
-    array_comprehension_exprt{array_comprehension_index,
-                              std::move(array_comprehension_body),
-                              to_array_type(src.type())},
+    array_comprehension_exprt{
+      array_comprehension_index,
+      std::move(array_comprehension_body),
+      to_array_type(src.type())},
     ns);
 }
 
@@ -1512,12 +1515,13 @@ static exprt lower_byte_update_byte_array_vector(
     if(non_const_update_bound.has_value())
     {
       update_value = typecast_exprt::conditional_cast(
-        if_exprt{binary_predicate_exprt{
-                   from_integer(i, non_const_update_bound->type()),
-                   ID_lt,
-                   *non_const_update_bound},
-                 element,
-                 index_exprt{src.op(), where}},
+        if_exprt{
+          binary_predicate_exprt{
+            from_integer(i, non_const_update_bound->type()),
+            ID_lt,
+            *non_const_update_bound},
+          element,
+          index_exprt{src.op(), where}},
         subtype);
     }
     else
@@ -1586,11 +1590,12 @@ static exprt lower_byte_update_array_vector_unbounded(
   // The actual value of updates other than at the start or end
   plus_exprt offset_expr{
     initial_bytes,
-    mult_exprt{subtype_size,
-               minus_exprt{typecast_exprt::conditional_cast(
-                             array_comprehension_index, first_index.type()),
-                           plus_exprt{first_index,
-                                      from_integer(1, first_index.type())}}}};
+    mult_exprt{
+      subtype_size,
+      minus_exprt{
+        typecast_exprt::conditional_cast(
+          array_comprehension_index, first_index.type()),
+        plus_exprt{first_index, from_integer(1, first_index.type())}}}};
   exprt update_value = lower_byte_extract(
     byte_extract_exprt{
       extract_opcode,
@@ -1605,21 +1610,24 @@ static exprt lower_byte_update_array_vector_unbounded(
   // below: (non_const_update_bound + (subtype_size - 1)) / subtype_size to
   // round up to the nearest multiple of subtype_size.
   div_exprt updated_elements{
-    plus_exprt{typecast_exprt::conditional_cast(
-                 non_const_update_bound, subtype_size.type()),
-               minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
+    plus_exprt{
+      typecast_exprt::conditional_cast(
+        non_const_update_bound, subtype_size.type()),
+      minus_exprt{subtype_size, from_integer(1, subtype_size.type())}},
     subtype_size};
 
   // The last element to be updated: first_index + updated_elements - 1
-  plus_exprt last_index{first_index,
-                        minus_exprt{std::move(updated_elements),
-                                    from_integer(1, first_index.type())}};
+  plus_exprt last_index{
+    first_index,
+    minus_exprt{
+      std::move(updated_elements), from_integer(1, first_index.type())}};
 
   // The size of a partial update at the end of the updated range, may be zero.
   mod_exprt tail_size{
-    minus_exprt{typecast_exprt::conditional_cast(
-                  non_const_update_bound, initial_bytes.type()),
-                initial_bytes},
+    minus_exprt{
+      typecast_exprt::conditional_cast(
+        non_const_update_bound, initial_bytes.type()),
+      initial_bytes},
     subtype_size};
 
   // The bound where updates end, which is conditional on the partial update
@@ -1628,9 +1636,10 @@ static exprt lower_byte_update_array_vector_unbounded(
     typecast_exprt::conditional_cast(
       array_comprehension_index, last_index.type()),
     ID_ge,
-    if_exprt{equal_exprt{tail_size, from_integer(0, tail_size.type())},
-             last_index,
-             plus_exprt{last_index, from_integer(1, last_index.type())}}};
+    if_exprt{
+      equal_exprt{tail_size, from_integer(0, tail_size.type())},
+      last_index,
+      plus_exprt{last_index, from_integer(1, last_index.type())}}};
 
   // The actual value of a partial update at the end.
   exprt last_update_value = lower_byte_update(
@@ -1648,20 +1657,24 @@ static exprt lower_byte_update_array_vector_unbounded(
     or_exprt{std::move(lower_bound), std::move(upper_bound)},
     index_exprt{src.op(), array_comprehension_index},
     if_exprt{
-      equal_exprt{typecast_exprt::conditional_cast(
-                    array_comprehension_index, first_index.type()),
-                  first_index},
+      equal_exprt{
+        typecast_exprt::conditional_cast(
+          array_comprehension_index, first_index.type()),
+        first_index},
       first_update_value,
-      if_exprt{equal_exprt{typecast_exprt::conditional_cast(
-                             array_comprehension_index, last_index.type()),
-                           last_index},
-               std::move(last_update_value),
-               std::move(update_value)}}};
+      if_exprt{
+        equal_exprt{
+          typecast_exprt::conditional_cast(
+            array_comprehension_index, last_index.type()),
+          last_index},
+        std::move(last_update_value),
+        std::move(update_value)}}};
 
   return simplify_expr(
-    array_comprehension_exprt{array_comprehension_index,
-                              std::move(array_comprehension_body),
-                              to_array_type(src.type())},
+    array_comprehension_exprt{
+      array_comprehension_index,
+      std::move(array_comprehension_body),
+      to_array_type(src.type())},
     ns);
 }
 
@@ -1718,10 +1731,10 @@ static exprt lower_byte_update_array_vector_non_const(
       "value should be an array expression if the update bound is constant");
     update_bound = update_size;
   }
-  initial_bytes =
-    if_exprt{binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
-             initial_bytes,
-             update_bound};
+  initial_bytes = if_exprt{
+    binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
+    initial_bytes,
+    update_bound};
   simplify(initial_bytes, ns);
 
   // encode the first update: update the original element at first_index (the
@@ -2060,8 +2073,9 @@ static exprt lower_byte_update_struct(
             *non_const_update_bound,
             ID_gt,
             from_integer(first, non_const_update_bound->type())},
-          minus_exprt{*non_const_update_bound,
-                      from_integer(first, non_const_update_bound->type())},
+          minus_exprt{
+            *non_const_update_bound,
+            from_integer(first, non_const_update_bound->type())},
           from_integer(0, non_const_update_bound->type())},
         size_type());
       // Now take the minimum of update-bytes-left and the previously computed
@@ -2110,10 +2124,11 @@ static exprt lower_byte_update_struct(
     {
       PRECONDITION(pointer_offset_bits(updated_element.type(), ns).has_value());
       elements.push_back(typecast_exprt::conditional_cast(
-        extractbits_exprt{updated_element,
-                          element_bits_int - 1 + (little_endian ? shift : 0),
-                          (little_endian ? shift : 0),
-                          bv_typet{element_bits_int}},
+        extractbits_exprt{
+          updated_element,
+          element_bits_int - 1 + (little_endian ? shift : 0),
+          (little_endian ? shift : 0),
+          bv_typet{element_bits_int}},
         comp.type()));
     }
 
@@ -2260,10 +2275,10 @@ static exprt lower_byte_update(
       typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
     if(bit_width > type_bits)
     {
-      val_before =
-        concatenation_exprt{from_integer(0, bv_typet{bit_width - type_bits}),
-                            val_before,
-                            bv_typet{bit_width}};
+      val_before = concatenation_exprt{
+        from_integer(0, bv_typet{bit_width - type_bits}),
+        val_before,
+        bv_typet{bit_width}};
 
       if(!is_little_endian)
         to_concatenation_expr(val_before)
@@ -2284,13 +2299,13 @@ static exprt lower_byte_update(
       CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
       for(std::size_t i = 0; i < update_bytes.size(); ++i)
       {
-        update_bytes[i] =
-          if_exprt{binary_predicate_exprt{
-                     from_integer(i, non_const_update_bound->type()),
-                     ID_lt,
-                     *non_const_update_bound},
-                   update_bytes[i],
-                   src_as_bytes.operands()[i]};
+        update_bytes[i] = if_exprt{
+          binary_predicate_exprt{
+            from_integer(i, non_const_update_bound->type()),
+            ID_lt,
+            *non_const_update_bound},
+          update_bytes[i],
+          src_as_bytes.operands()[i]};
       }
     }
 
@@ -2485,7 +2500,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
 
 exprt lower_byte_operators(const exprt &src, const namespacet &ns)
 {
-  exprt tmp=src;
+  exprt tmp = src;
 
   // destroys any sharing, should use hash table
   Forall_operands(it, tmp)
@@ -2493,12 +2508,18 @@ exprt lower_byte_operators(const exprt &src, const namespacet &ns)
     *it = lower_byte_operators(*it, ns);
   }
 
-  if(src.id()==ID_byte_update_little_endian ||
-     src.id()==ID_byte_update_big_endian)
+  if(
+    src.id() == ID_byte_update_little_endian ||
+    src.id() == ID_byte_update_big_endian)
+  {
     return lower_byte_update(to_byte_update_expr(tmp), ns);
-  else if(src.id()==ID_byte_extract_little_endian ||
-          src.id()==ID_byte_extract_big_endian)
+  }
+  else if(
+    src.id() == ID_byte_extract_little_endian ||
+    src.id() == ID_byte_extract_big_endian)
+  {
     return lower_byte_extract(to_byte_extract_expr(tmp), ns);
+  }
   else
     return tmp;
 }
diff --git a/unit/Makefile b/unit/Makefile
index fb02559566d..2b49983112c 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -94,7 +94,6 @@ SRC += analyses/ai/ai.cpp \
        pointer-analysis/value_set.cpp \
        solvers/bdd/miniBDD/miniBDD.cpp \
        solvers/floatbv/float_utils.cpp \
-       solvers/lowering/byte_operators.cpp \
        solvers/prop/bdd_expr.cpp \
        solvers/sat/external_sat.cpp \
        solvers/sat/satcheck_cadical.cpp \
@@ -159,6 +158,7 @@ SRC += analyses/ai/ai.cpp \
        util/json_array.cpp \
        util/json_object.cpp \
        util/lazy.cpp \
+       util/lower_byte_operators.cpp \
        util/memory_info.cpp \
        util/message.cpp \
        util/optional.cpp \
diff --git a/unit/solvers/lowering/module_dependencies.txt b/unit/solvers/lowering/module_dependencies.txt
deleted file mode 100644
index 146b6f0220c..00000000000
--- a/unit/solvers/lowering/module_dependencies.txt
+++ /dev/null
@@ -1,3 +0,0 @@
-solvers/lowering
-testing-utils
-util
diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/util/lower_byte_operators.cpp
similarity index 98%
rename from unit/solvers/lowering/byte_operators.cpp
rename to unit/util/lower_byte_operators.cpp
index dbf81fbdf3f..59c384b24c4 100644
--- a/unit/solvers/lowering/byte_operators.cpp
+++ b/unit/util/lower_byte_operators.cpp
@@ -6,10 +6,6 @@
 
 \*******************************************************************/
 
-#include <testing-utils/use_catch.h>
-
-#include <solvers/lowering/expr_lowering.h>
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
@@ -24,7 +20,9 @@
 #include <util/string_constant.h>
 #include <util/symbol_table.h>
 
-TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("byte extract and bits", "[core][util][lowering][byte_extract]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness
@@ -94,7 +92,7 @@ TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
   }
 }
 
-SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
+SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness
@@ -362,7 +360,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
   }
 }
 
-SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
+SCENARIO("byte_update_lowering", "[core][util][lowering][byte_update]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness