From 634bb4bf1b1d8c98dc45bbd8f540730a916a7c9e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 28 Oct 2026 08:45:04 +0000
Subject: [PATCH] SMT2: parse values of bit-fields

smt2_convt::parse_rec had no case for c_bit_field types and returned
nil, so traces showed bit-field members as "(assignment removed)".
Parse the value using the integer type of the bit-field's width and
signedness (c_bit_field_replacement_type), and restore the bit-field
type.

This only affects counterexample traces of the SMT2 back ends, not
verification results.

Reported by Jeroen Robben (https://reports.robben.io/methodology/).

Fixes #9346

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 regression/cbmc/smt2-bitfield-trace/main.c    | 15 +++++++++++++++
 regression/cbmc/smt2-bitfield-trace/test.desc | 10 ++++++++++
 src/solvers/smt2/smt2_conv.cpp                | 10 ++++++++++
 3 files changed, 35 insertions(+)
 create mode 100644 regression/cbmc/smt2-bitfield-trace/main.c
 create mode 100644 regression/cbmc/smt2-bitfield-trace/test.desc

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)