diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
index e84e0d96599c..2175971a8824 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.cpp
+++ b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -40,7 +40,6 @@ Author: Peter Schrammel
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
@@ -296,7 +295,6 @@ bool jdiff_parse_optionst::process_goto_program(
     remove_returns(goto_model);
     remove_vector(goto_model);
     remove_complex(goto_model);
-    rewrite_union(goto_model);
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;
diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel
index 2ba432c93b36..b9bdd513da6e 100644
Binary files a/regression/ansi-c/arch_flags_mcpu_bad/object.intel and b/regression/ansi-c/arch_flags_mcpu_bad/object.intel differ
diff --git a/regression/ansi-c/arch_flags_mcpu_bad/test.desc b/regression/ansi-c/arch_flags_mcpu_bad/test.desc
index 5b43f9022cfd..2cfda406b60a 100644
--- a/regression/ansi-c/arch_flags_mcpu_bad/test.desc
+++ b/regression/ansi-c/arch_flags_mcpu_bad/test.desc
@@ -11,7 +11,7 @@ This tests the -mcpu=cortex=a15 flag that should activate ARM-32 mode.
 The object file 'object.intel' was compiled from 'source.c' with goto-cc
 on a 64-bit platform:
 
-  goto-cc -c source.c
+  goto-cc -c source.c -o object.intel
 
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm
index 6593905c6b48..cfd8751c1893 100644
Binary files a/regression/ansi-c/arch_flags_mcpu_good/object.arm and b/regression/ansi-c/arch_flags_mcpu_good/object.arm differ
diff --git a/regression/ansi-c/arch_flags_mthumb_bad/object.intel b/regression/ansi-c/arch_flags_mthumb_bad/object.intel
index d1b887e5bef2..e6a6b5e2bd53 100644
Binary files a/regression/ansi-c/arch_flags_mthumb_bad/object.intel and b/regression/ansi-c/arch_flags_mthumb_bad/object.intel differ
diff --git a/regression/ansi-c/arch_flags_mthumb_bad/test.desc b/regression/ansi-c/arch_flags_mthumb_bad/test.desc
index f163942b27f9..2a1c9d3ea88f 100644
--- a/regression/ansi-c/arch_flags_mthumb_bad/test.desc
+++ b/regression/ansi-c/arch_flags_mthumb_bad/test.desc
@@ -11,7 +11,7 @@ This tests the -mthumb flag that should activate ARM-32 mode. The object
 file 'object.intel' was compiled from 'source.c' with goto-cc on a
 64-bit platform:
 
-  goto-cc -c source.c
+  goto-cc -c source.c -o object.intel
 
 preproc.i is already pre-processed so that it can be linked in without
 needing to invoke a pre-processor from a cross-compile toolchain on your
diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm
index 6a398a5058be..9e725a7a4a84 100644
Binary files a/regression/ansi-c/arch_flags_mthumb_good/object.arm and b/regression/ansi-c/arch_flags_mthumb_good/object.arm differ
diff --git a/regression/cbmc-library/float-nan-check/test.desc b/regression/cbmc-library/float-nan-check/test.desc
index f90dd750bf59..7c4679b52541 100644
--- a/regression/cbmc-library/float-nan-check/test.desc
+++ b/regression/cbmc-library/float-nan-check/test.desc
@@ -1,15 +1,15 @@
 CORE
 main.c
 --nan-check
-\[main.NaN.1\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ myzero: SUCCESS
+\[main.NaN.1\] line \d+ NaN on \+ in c\.f \+ myzero: SUCCESS
 \[main.NaN.2\] line \d+ NaN on / in myzero / myzero: FAILURE
 \[main.NaN.3\] line \d+ NaN on / in \(float\)n / myinf: FAILURE
 \[main.NaN.4\] line \d+ NaN on \* in myinf \* myzero: FAILURE
 \[main.NaN.5\] line \d+ NaN on \+ in -myinf \+ myinf: FAILURE
 \[main.NaN.6\] line \d+ NaN on - in myinf - myinf: FAILURE
 \[main.NaN.7\] line \d+ NaN on - in -myinf - -myinf: FAILURE
-\[main.NaN.8\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ byte_extract_little_endian\(c, (0|0l|0ll), float\): SUCCESS
-\[main.NaN.9\] line \d+ NaN on / in byte_extract_little_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS
+\[main.NaN.8\] line \d+ NaN on \+ in c\.f \+ c\.f: SUCCESS
+\[main.NaN.9\] line \d+ NaN on / in c\.f / myzero: SUCCESS
 \[main.NaN.10\] line \d+ NaN on \* in mynan \* mynan: SUCCESS
 \[main.NaN.11\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS
 \[main.NaN.12\] line \d+ NaN on - in mynan - mynan: SUCCESS
diff --git a/regression/cbmc/union7/no_simplify.desc b/regression/cbmc/union7/no_simplify.desc
new file mode 100644
index 000000000000..34a9fb409183
--- /dev/null
+++ b/regression/cbmc/union7/no_simplify.desc
@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+main.c
+--big-endian --no-simplify
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Although this test can now be fully solved via constant propagation and
+simplification, it should also succeed without simplification.
diff --git a/regression/cbmc/union7/test.desc b/regression/cbmc/union7/test.desc
index 58448e0655b0..b33c7528f52e 100644
--- a/regression/cbmc/union7/test.desc
+++ b/regression/cbmc/union7/test.desc
@@ -1,11 +1,11 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
+Generated 3 VCC\(s\), 0 remaining after simplification
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
 --
-This test reports a VERIFICATION ERROR when running with the SMT2 solver on
-Windows only.
+This test can now be fully solved via constant propagation and simplification.
diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc
index cf2fe7e81357..5913aa431d20 100644
--- a/regression/cbmc/xml-trace/test.desc
+++ b/regression/cbmc/xml-trace/test.desc
@@ -7,7 +7,7 @@ VERIFICATION FAILED
 <assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">
 <location file=".*" function="test" line="\d+" working-directory=".*"/>
 <type>union myunion</type>
-<full_lhs>byte_extract_little_endian\(u, 0ll?, .*int.*\)</full_lhs>
+<full_lhs>u</full_lhs>
 <full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>
 <value>\{ \.i=\d+ll? \}</value>
 <value_expression>
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
index 2766e483dc57..80a3b19fa271 100644
--- a/scripts/expected_doxygen_warnings.txt
+++ b/scripts/expected_doxygen_warnings.txt
@@ -79,13 +79,13 @@
 /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp:188: warning: The following parameter of initialize_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns, const vsd_configt &configuration) is not documented:
   parameter 'configuration'
 
-warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index a59a541f801e..ecd228fb93cd 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_initializer.h>
 #include <util/expr_util.h>
 #include <util/ieee_float.h>
 #include <util/mathematical_expr.h>
@@ -1086,6 +1087,36 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
         expr.set(ID_C_lvalue, true);
         return;
       }
+      else if(c.get_anonymous() && c.type().id() == ID_struct_tag)
+      {
+        // we also look into anonymous members as we might have wrapped a
+        // non-maximal member in such a struct
+        const struct_typet &struct_type =
+          follow_tag(to_struct_tag_type(c.type()));
+        if(
+          !struct_type.components().empty() &&
+          struct_type.components().front().type() == op.type())
+        {
+          auto nondet =
+            nondet_initializer(c.type(), expr.source_location(), *this);
+          if(!nondet.has_value())
+          {
+            error().source_location = expr.source_location();
+            error() << "cannot nondet-initialize union component of type '"
+                    << to_string(c.type()) << "'" << eom;
+            throw 0;
+          }
+          CHECK_RETURN(nondet->id() == ID_struct);
+          CHECK_RETURN(!nondet->operands().empty());
+
+          nondet->operands().front() = op;
+          union_exprt union_expr(c.get_name(), *nondet, expr.type());
+          union_expr.add_source_location() = expr.source_location();
+          expr = union_expr;
+          expr.set(ID_C_lvalue, true);
+          return;
+        }
+      }
     }
 
     // not found, complain
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index bf82c39bdca9..b1937535733f 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -530,27 +530,36 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         // initializer; other bytes have an unspecified value (C Standard
         // 6.2.6.1(7)). In practice, objects of static lifetime are fully zero
         // initialized.
-        const auto zero =
-          zero_initializer(component.type(), value.source_location(), *this);
-        if(!zero.has_value())
-        {
-          error().source_location = value.source_location();
-          error() << "cannot zero-initialize union component of type '"
-                  << to_string(component.type()) << "'" << eom;
-          throw 0;
-        }
-
         if(current_symbol.is_static_lifetime)
         {
-          byte_update_exprt byte_update{
-            byte_update_id(), *dest, from_integer(0, index_type()), *zero};
-          byte_update.add_source_location() = value.source_location();
-          *dest = std::move(byte_update);
-          dest = &(to_byte_update_expr(*dest).op2());
+          const auto zero =
+            zero_initializer(component.type(), value.source_location(), *this);
+          if(!zero.has_value())
+          {
+            error().source_location = value.source_location();
+            error() << "cannot zero-initialize union component of type '"
+                    << to_string(component.type()) << "'" << eom;
+            throw 0;
+          }
+
+          union_exprt union_expr(component.get_name(), *zero, type);
+          union_expr.add_source_location() = value.source_location();
+          *dest = std::move(union_expr);
+          dest = &(to_union_expr(*dest).op());
         }
         else
         {
-          union_exprt union_expr(component.get_name(), *zero, type);
+          const auto nondet = nondet_initializer(
+            component.type(), value.source_location(), *this);
+          if(!nondet.has_value())
+          {
+            error().source_location = value.source_location();
+            error() << "cannot nondet-initialize union component of type '"
+                    << to_string(component.type()) << "'" << eom;
+            throw 0;
+          }
+
+          union_exprt union_expr(component.get_name(), *nondet, type);
           union_expr.add_source_location() = value.source_location();
           *dest = std::move(union_expr);
           dest = &(to_union_expr(*dest).op());
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index d7bcda5a11da..5e45738d4525 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1072,6 +1072,134 @@ void c_typecheck_baset::typecheck_compound_body(
     else
       it++;
   }
+
+  if(type.id() == ID_union && !components.empty())
+  {
+    const auto widest_member =
+      to_union_type(type).find_widest_union_component(*this);
+    optionalt<exprt> size_expr_opt;
+
+    if(!widest_member.has_value())
+    {
+      // GCC extension: arrays of non-constant size
+      size_expr_opt = size_of_expr(type, *this);
+
+      if(!size_expr_opt.has_value())
+      {
+        error().source_location = type.source_location();
+        error() << "cannot determine size of union" << eom;
+        throw 0;
+      }
+    }
+
+    for(auto &component : components)
+    {
+      std::vector<typet> padding_types;
+
+      const auto &component_bits = pointer_offset_bits(component.type(), *this);
+      if(
+        component_bits.has_value() &&
+        (!widest_member.has_value() ||
+         *component_bits < widest_member->second) &&
+        *component_bits % 8 != 0)
+      {
+        std::size_t bit_field_padding_width =
+          8 - numeric_cast_v<std::size_t>(*component_bits % 8);
+        padding_types.push_back(c_bit_field_typet{
+          unsignedbv_typet{bit_field_padding_width}, bit_field_padding_width});
+      }
+
+      if(size_expr_opt.has_value())
+      {
+        const auto component_size_expr_opt =
+          size_of_expr(component.type(), *this);
+        CHECK_RETURN(component_size_expr_opt.has_value());
+        // size_of_expr will round up to full bytes, and also works for bit
+        // fields (which C sizeof does not support). Thus, we don't need to
+        // special-case bit_field_padding_opt being set.
+        if_exprt padding_bytes{
+          binary_relation_exprt{
+            *component_size_expr_opt, ID_lt, *size_expr_opt},
+          minus_exprt{*size_expr_opt, *component_size_expr_opt},
+          from_integer(0, size_expr_opt->type())};
+        simplify(padding_bytes, *this);
+
+        if(!padding_bytes.is_zero())
+        {
+          make_index_type(padding_bytes);
+
+          padding_types.push_back(
+            array_typet{unsigned_char_type(), padding_bytes});
+        }
+      }
+      else
+      {
+        CHECK_RETURN(component_bits.has_value());
+        // Truncating division ensures that we don't need to special-case
+        // bit_field_padding_opt being set.
+        std::size_t padding_bytes =
+          numeric_cast_v<std::size_t>(widest_member->second - *component_bits) /
+          8;
+
+        if(padding_bytes != 0)
+        {
+          padding_types.push_back(array_typet{
+            unsigned_char_type(), from_integer(padding_bytes, index_type())});
+        }
+      }
+
+      if(padding_types.empty())
+        continue;
+
+      struct_typet::componentst component_with_padding_type;
+      component_with_padding_type.push_back(component);
+      for(const auto &t : padding_types)
+      {
+        // TODO: perhaps use the same naming as padding.cpp uses
+        component_with_padding_type.push_back(struct_union_typet::componentt{
+          "$anon" + std::to_string(anon_member_counter++), t});
+        // TODO: not sure whether this should be anonymous
+        component_with_padding_type.back().set_anonymous(true);
+        component_with_padding_type.back().set_is_padding(true);
+        component_with_padding_type.back().add_source_location() =
+          component.source_location();
+      }
+
+      struct_union_typet::componentt component_with_padding{
+        "$anon" + std::to_string(anon_member_counter++),
+        struct_typet{component_with_padding_type}};
+      component_with_padding.set_anonymous(true);
+      component_with_padding.add_source_location() =
+        component.source_location();
+
+      // based on typecheck_compound_type, branch
+      // "if(type.find(ID_tag).is_nil())"
+      // produce type symbol
+      type_symbolt compound_symbol{component_with_padding.type()};
+      compound_symbol.location = component_with_padding.source_location();
+
+      std::string typestr = type2name(compound_symbol.type, *this);
+      compound_symbol.base_name = "#anon#" + typestr;
+      compound_symbol.name = "tag-#anon#" + typestr;
+
+      // We might already have the same anonymous struct, and this is simply
+      // ok as those are exactly the same types, just introduced at a
+      // different source location.
+      symbolt *new_symbol = &compound_symbol;
+      if(
+        symbol_table.symbols.find(compound_symbol.name) ==
+        symbol_table.symbols.end())
+      {
+        move_symbol(compound_symbol, new_symbol);
+      }
+
+      struct_tag_typet tag_type{new_symbol->name};
+      tag_type.add_source_location() = component_with_padding.source_location();
+      component_with_padding.type().swap(tag_type);
+
+      component.swap(component_with_padding);
+    }
+  }
 }
 
 typet c_typecheck_baset::enum_constant_type(
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 48ff28ae69ef..2a3a076b9209 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -62,7 +62,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
-#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
@@ -943,7 +942,6 @@ bool cbmc_parse_optionst::process_goto_program(
   remove_returns(goto_model);
   remove_vector(goto_model);
   remove_complex(goto_model);
-  rewrite_union(goto_model);
 
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index f0478bd24c4d..d0a3b0d60494 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -40,7 +40,6 @@ Author: Peter Schrammel
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/rewrite_union.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
@@ -341,7 +340,6 @@ bool goto_diff_parse_optionst::process_goto_program(
     remove_returns(goto_model);
     remove_vector(goto_model);
     remove_complex(goto_model);
-    rewrite_union(goto_model);
 
     // add generic checks
     log.status() << "Generic Property Instrumentation" << messaget::eom;
diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h
index a770e7bd3912..13a3996a9bdc 100644
--- a/src/goto-programs/write_goto_binary.h
+++ b/src/goto-programs/write_goto_binary.h
@@ -12,7 +12,7 @@ Author: CM Wintersteiger
 #ifndef CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
 #define CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
 
-#define GOTO_BINARY_VERSION 5
+#define GOTO_BINARY_VERSION 6
 
 #include <iosfwd>
 #include <string>
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index f533be10855b..122770699522 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -54,9 +54,7 @@ void symex_assignt::assign_rec(
     }
     else if(type.id() == ID_union || type.id() == ID_union_tag)
     {
-      // should have been replaced by byte_extract
-      throw unsupported_operation_exceptiont(
-        "assign_rec: unexpected assignment to union member");
+      assign_union_member(to_member_expr(lhs), full_lhs, rhs, guard);
     }
     else
       throw unsupported_operation_exceptiont(
@@ -343,6 +341,30 @@ void symex_assignt::assign_struct_member(
   }
 }
 
+void symex_assignt::assign_union_member(
+  const member_exprt &lhs,
+  const expr_skeletont &full_lhs,
+  const exprt &rhs,
+  exprt::operandst &guard)
+{
+  // Symbolic execution of a union member assignment.
+
+  // lhs must be member operand, which takes one operand, which must be a union.
+  exprt lhs_union = lhs.op();
+  const irep_idt &component_name = lhs.get_component_name();
+
+  // turn
+  //   a.c=e
+  // into
+  //   a'== { .c=e }
+  // as the front-end guarantees that .c will have the full size of the union
+
+  union_exprt new_rhs{component_name, rhs, lhs_union.type()};
+  const expr_skeletont new_skeleton =
+    full_lhs.compose(expr_skeletont::remove_op0(lhs));
+  assign_rec(lhs_union, new_skeleton, new_rhs, guard);
+}
+
 void symex_assignt::assign_if(
   const if_exprt &lhs,
   const expr_skeletont &full_lhs,
diff --git a/src/goto-symex/symex_assign.h b/src/goto-symex/symex_assign.h
index 7e3cff721d35..16cf58ecc5a4 100644
--- a/src/goto-symex/symex_assign.h
+++ b/src/goto-symex/symex_assign.h
@@ -92,6 +92,12 @@ class symex_assignt
     const exprt &rhs,
     exprt::operandst &guard);
 
+  void assign_union_member(
+    const member_exprt &lhs,
+    const expr_skeletont &full_lhs,
+    const exprt &rhs,
+    exprt::operandst &guard);
+
   void assign_if(
     const if_exprt &lhs,
     const expr_skeletont &full_lhs,
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 976e06c32c8f..7d6d51bc81d6 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -783,6 +783,11 @@ void value_sett::get_value_set_rec(
         get_value_set_rec(*it, dest, suffix, original_type, ns);
     }
   }
+  else if(expr.id() == ID_union)
+  {
+    get_value_set_rec(
+      to_union_expr(expr).op(), dest, suffix, original_type, ns);
+  }
   else if(expr.id()==ID_with)
   {
     const with_exprt &with_expr = to_with_expr(expr);
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index 6a78dda8609f..e9f3fd5796b7 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/src/solvers/flattening/boolbv_member.cpp
@@ -8,16 +8,22 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-bvt boolbvt::convert_member(const member_exprt &expr)
+#include <util/config.h>
+
+#include "bv_endianness_map.h"
+
+static bvt convert_member_struct(
+  const member_exprt &expr,
+  const bvt &struct_bv,
+  const boolbv_widtht &boolbv_width,
+  const namespacet &ns)
 {
   const exprt &struct_op=expr.struct_op();
   const typet &struct_op_type=ns.follow(struct_op.type());
 
-  const bvt &struct_bv=convert_bv(struct_op);
-
   const irep_idt &component_name = expr.get_component_name();
-  const struct_union_typet::componentst &components =
-    to_struct_union_type(struct_op_type).components();
+  const struct_typet::componentst &components =
+    to_struct_type(struct_op_type).components();
 
   std::size_t offset = 0;
 
@@ -42,8 +48,7 @@ bvt boolbvt::convert_member(const member_exprt &expr)
         struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
     }
 
-    if(struct_op_type.id() != ID_union)
-      offset += sub_width;
+    offset += sub_width;
   }
 
   INVARIANT_WITH_DIAGNOSTICS(
@@ -52,3 +57,60 @@ bvt boolbvt::convert_member(const member_exprt &expr)
     expr.find_source_location(),
     id2string(component_name));
 }
+
+static bvt convert_member_union(
+  const member_exprt &expr,
+  const bvt &union_bv,
+  const boolbv_widtht &boolbv_width,
+  const namespacet &ns)
+{
+  const exprt &union_op = expr.compound();
+  const union_typet &union_op_type =
+    ns.follow_tag(to_union_tag_type(union_op.type()));
+
+  const irep_idt &component_name = expr.get_component_name();
+  const union_typet::componentt &component =
+    union_op_type.get_component(component_name);
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    component.is_not_nil(),
+    "union type shall contain component accessed by member expression",
+    expr.find_source_location(),
+    id2string(component_name));
+
+  const typet &subtype = component.type();
+  const std::size_t sub_width = boolbv_width(subtype);
+
+  if(
+    config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
+  {
+    return bvt(union_bv.begin(), union_bv.begin() + sub_width);
+  }
+  else
+  {
+    DATA_INVARIANT(
+      config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_BIG_ENDIAN,
+      "endianness should be configured to little or big endian");
+
+    bv_endianness_mapt map_u(union_op_type, false, ns, boolbv_width);
+    bv_endianness_mapt map_component(subtype, false, ns, boolbv_width);
+
+    bvt result(sub_width, literalt{});
+    for(std::size_t i = 0; i < sub_width; ++i)
+      result[map_u.map_bit(i)] = union_bv[map_component.map_bit(i)];
+
+    return result;
+  }
+}
+
+bvt boolbvt::convert_member(const member_exprt &expr)
+{
+  const bvt &compound_bv = convert_bv(expr.compound());
+
+  if(expr.compound().type().id() == ID_struct_tag)
+    return convert_member_struct(expr, compound_bv, boolbv_width, ns);
+  else
+  {
+    PRECONDITION(expr.compound().type().id() == ID_union_tag);
+    return convert_member_union(expr, compound_bv, boolbv_width, ns);
+  }
+}
diff --git a/src/solvers/flattening/bv_endianness_map.h b/src/solvers/flattening/bv_endianness_map.h
index d15f3d463b29..ed16567345d4 100644
--- a/src/solvers/flattening/bv_endianness_map.h
+++ b/src/solvers/flattening/bv_endianness_map.h
@@ -24,14 +24,14 @@ class bv_endianness_mapt : public endianness_mapt
     const typet &type,
     bool little_endian,
     const namespacet &_ns,
-    boolbv_widtht &_boolbv_width)
+    const boolbv_widtht &_boolbv_width)
     : endianness_mapt(_ns), boolbv_width(_boolbv_width)
   {
     build(type, little_endian);
   }
 
 protected:
-  boolbv_widtht &boolbv_width;
+  const boolbv_widtht &boolbv_width;
 
   virtual void build_little_endian(const typet &type) override;
   virtual void build_big_endian(const typet &type) override;
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 9a8afc584852..bd46dacf21e9 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 #include "byte_operators.h"
+#include "c_types.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
@@ -184,26 +185,16 @@ simplify_exprt::simplify_member(const member_exprt &expr)
     if(to_union_expr(op).op().type() == expr.type())
       return to_union_expr(op).op();
 
-    // need to convert!
-    auto target_size = pointer_offset_size(expr.type(), ns);
-
-    if(target_size.has_value())
-    {
-      mp_integer target_bits = target_size.value() * 8;
-      const auto bits = expr2bits(op, true, ns);
-
-      if(bits.has_value() &&
-         mp_integer(bits->size())>=target_bits)
-      {
-        std::string bits_cut =
-          std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
-
-        auto tmp = bits2expr(bits_cut, expr.type(), true, ns);
-
-        if(tmp.has_value())
-          return std::move(*tmp);
-      }
-    }
+    // need to convert, taking endianness into account
+    byte_extract_exprt byte_extract{
+      byte_extract_id(), op, from_integer(0, index_type()), expr.type()};
+    // try to simplify this, but never return the byte_extract expression to
+    // avoid infinite rewrite loops
+    auto result = simplify_byte_extract(byte_extract);
+    if(result.expr.id() != byte_extract_id())
+      return result;
+    else
+      return unchanged(expr);
   }
   else if(op.id() == ID_typecast)
   {