diff --git a/regression/cbmc/smt2-bitfield-trace/main.c b/regression/cbmc/smt2-bitfield-trace/main.c
new file mode 100644
index 00000000000..7a79bb447cb
--- /dev/null
+++ b/regression/cbmc/smt2-bitfield-trace/main.c
@@ -0,0 +1,15 @@
+unsigned nondet_u(void);
+struct S
+{
+  unsigned bf : 3;
+  unsigned other;
+};
+int main(void)
+{
+  struct S s;
+  s.bf = nondet_u();
+  s.other = 7;
+  __CPROVER_assume(s.bf == 5);
+  __CPROVER_assert(0, "show trace");
+  return 0;
+}
diff --git a/regression/cbmc/smt2-bitfield-trace/test.desc b/regression/cbmc/smt2-bitfield-trace/test.desc
new file mode 100644
index 00000000000..cdc82de88cb
--- /dev/null
+++ b/regression/cbmc/smt2-bitfield-trace/test.desc
@@ -0,0 +1,10 @@
+CORE no-new-smt
+main.c
+--trace --z3
+^EXIT=10$
+^SIGNAL=0$
+^  s\.bf=5u
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+assignment removed
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index a809ebf9b10..a89f804aa34 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -789,6 +789,16 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
   {
     return parse_literal(src, type);
   }
+  else if(type.id() == ID_c_bit_field)
+  {
+    // bit-fields are bit vectors of their width: parse them using the
+    // corresponding integer type
+    exprt result = parse_rec(
+      src, c_bit_field_replacement_type(to_c_bit_field_type(type), ns));
+    if(result.is_not_nil())
+      result.type() = type;
+    return result;
+  }
   else if(type.id()==ID_bool)
   {
     if(src.id()==ID_1 || src.id()==ID_true)