diff --git a/regression/cbmc/byte_update_sub_byte1/main.c b/regression/cbmc/byte_update_sub_byte1/main.c
new file mode 100644
index 00000000000..c9e9b0139f2
--- /dev/null
+++ b/regression/cbmc/byte_update_sub_byte1/main.c
@@ -0,0 +1,7 @@
+int main()
+{
+  unsigned x;
+  __CPROVER_bitvector[1] *p = (__CPROVER_bitvector[1] *)&x;
+  *p = 0;
+  __CPROVER_assert((x & 0x80u) == 0u, "MSB of byte 0 is cleared");
+}
diff --git a/regression/cbmc/byte_update_sub_byte1/symbolic-offset.desc b/regression/cbmc/byte_update_sub_byte1/symbolic-offset.desc
new file mode 100644
index 00000000000..f33a24a3106
--- /dev/null
+++ b/regression/cbmc/byte_update_sub_byte1/symbolic-offset.desc
@@ -0,0 +1,11 @@
+CORE
+symbolic.c
+--little-endian --no-simplify
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Same as test.desc but with a symbolic (constrained-to-0) byte offset,
+exercising the variable-offset branch of convert_byte_update.
diff --git a/regression/cbmc/byte_update_sub_byte1/symbolic.c b/regression/cbmc/byte_update_sub_byte1/symbolic.c
new file mode 100644
index 00000000000..5b6d35c64b3
--- /dev/null
+++ b/regression/cbmc/byte_update_sub_byte1/symbolic.c
@@ -0,0 +1,9 @@
+int main()
+{
+  unsigned x;
+  unsigned offset;
+  __CPROVER_assume(offset == 0);
+  __CPROVER_bitvector[1] *p = (__CPROVER_bitvector[1] *)((char *)&x + offset);
+  *p = 0;
+  __CPROVER_assert((x & 0x80u) == 0u, "MSB of byte 0 is cleared");
+}
diff --git a/regression/cbmc/byte_update_sub_byte1/test.desc b/regression/cbmc/byte_update_sub_byte1/test.desc
new file mode 100644
index 00000000000..003c42029e8
--- /dev/null
+++ b/regression/cbmc/byte_update_sub_byte1/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--little-endian --no-simplify
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Writing a 1-bit zero through a __CPROVER_bitvector[1] pointer must
+clear the MSB of the first byte, not the LSB. The --no-simplify flag
+is needed to exercise the boolbv convert_byte_update path directly.
+This test uses a constant offset (byte 0).
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 3d94761b5a8..c101712d24d 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -41,6 +41,22 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   if(update_width>bv.size())
     update_width=bv.size();
 
+  // When the update value is not a multiple of the byte width,
+  // lower_byte_update places the value at the high end of the last partial
+  // byte (concatenating {value, remaining_low_bits}). For little-endian the
+  // high end is at higher bit indices, so we shift the trailing partial
+  // byte's bits up. For big-endian the endianness map already places bit 0
+  // at the MSB, so no shift is needed.
+  const std::size_t tail_bits = update_width % byte_width;
+  const std::size_t tail_shift =
+    little_endian && tail_bits != 0 ? byte_width - tail_bits : 0;
+
+  // For a given bit index i (0-based within the update value), compute the
+  // additional offset to place trailing partial-byte bits at the high end.
+  auto bit_shift = [&](std::size_t i) -> std::size_t {
+    return (tail_shift != 0 && i >= update_width - tail_bits) ? tail_shift : 0;
+  };
+
   // see if the byte number is constant
 
   const auto index = numeric_cast<mp_integer>(offset_expr);
@@ -62,7 +78,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 
       for(std::size_t i = 0; i < update_width; i++)
       {
-        size_t index_op = map_op.map_bit(offset_i + i);
+        size_t index_op = map_op.map_bit(offset_i + bit_shift(i) + i);
         size_t index_value = map_value.map_bit(i);
 
         INVARIANT(
@@ -90,9 +106,9 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
     endianness_mapt map_value = endianness_map(value.type(), little_endian);
 
     for(std::size_t bit=0; bit<update_width; bit++)
-      if(offset+bit<bv.size())
+      if(offset + bit_shift(bit) + bit < bv.size())
       {
-        std::size_t bv_o=map_op.map_bit(offset+bit);
+        std::size_t bv_o = map_op.map_bit(offset + bit_shift(bit) + bit);
         std::size_t value_bv_o=map_value.map_bit(bit);
 
         bv[bv_o]=prop.lselect(equal, value_bv[value_bv_o], bv[bv_o]);