From 5c8198811821ff2e67be3325b4831a2c537ab149 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 20 Oct 2026 18:04:35 +0000
Subject: [PATCH] SAT: use c_enum underlying type signedness for extensions

The SAT back end (boolbv_typecast) treated all c_enum values as signed
when extending to wider types: integer-to-integer, integer-to-fixedbv,
and integer-to-float conversions all used sign extension for c_enum
sources. This is wrong for enums whose underlying type is unsigned
(e.g., enums with values > INT_MAX or packed enums with values > 127).

Fix: check the c_enum underlying type signedness in all three places
instead of unconditionally treating IS_C_ENUM as signed.

Fixes #9206

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 regression/cbmc/enum_unsigned_widen/main.c    | 28 +++++++++++++++++++
 regression/cbmc/enum_unsigned_widen/test.desc |  8 ++++++
 src/solvers/flattening/boolbv_typecast.cpp    | 22 +++++++++++++--
 3 files changed, 55 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/enum_unsigned_widen/main.c
 create mode 100644 regression/cbmc/enum_unsigned_widen/test.desc

diff --git a/regression/cbmc/enum_unsigned_widen/main.c b/regression/cbmc/enum_unsigned_widen/main.c
new file mode 100644
index 000000000000..937df433a5c6
--- /dev/null
+++ b/regression/cbmc/enum_unsigned_widen/main.c
@@ -0,0 +1,28 @@
+enum E
+{
+  A = 0x80000000u,
+  B = 1
+};
+enum __attribute__((packed)) P
+{
+  X = 200,
+  Y = 1
+};
+enum E nondet_e(void);
+enum P nondet_p(void);
+
+int main(void)
+{
+  // enum E has underlying type unsigned int
+  enum E e = nondet_e();
+  __CPROVER_assume(e == A || e == B);
+  long long l = e;
+  __CPROVER_assert(l > 0, "unsigned enum widened is positive");
+
+  // enum P has underlying type unsigned char
+  enum P p = nondet_p();
+  __CPROVER_assume(p == X);
+  int i = p;
+  __CPROVER_assert(i == 200, "packed unsigned enum converts correctly");
+  return 0;
+}
diff --git a/regression/cbmc/enum_unsigned_widen/test.desc b/regression/cbmc/enum_unsigned_widen/test.desc
new file mode 100644
index 000000000000..749292d9497d
--- /dev/null
+++ b/regression/cbmc/enum_unsigned_widen/test.desc
@@ -0,0 +1,8 @@
+CORE broken-cprover-smt-backend gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index 64c82b1e0ac9..2301c668027a 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -182,11 +182,24 @@ bool boolbvt::type_conversion(
       break;
 
     case bvtypet::IS_SIGNED: // signed to float
-    case bvtypet::IS_C_ENUM:
       float_utils.spec = ieee_float_spect(to_floatbv_type(dest_type));
       dest = float_utils.from_signed_integer(src);
       return false;
 
+    case bvtypet::IS_C_ENUM: // enum to float
+      float_utils.spec = ieee_float_spect(to_floatbv_type(dest_type));
+      if(
+        src_type.id() == ID_c_enum &&
+        to_c_enum_type(src_type).underlying_type().id() == ID_unsignedbv)
+      {
+        dest = float_utils.from_unsigned_integer(src);
+      }
+      else
+      {
+        dest = float_utils.from_signed_integer(src);
+      }
+      return false;
+
     case bvtypet::IS_UNSIGNED: // unsigned to float
     case bvtypet::IS_C_BOOL:   // _Bool to float
       float_utils.spec = ieee_float_spect(to_floatbv_type(dest_type));
@@ -298,7 +311,8 @@ bool boolbvt::type_conversion(
         {
           if(
             src_bvtype == bvtypet::IS_SIGNED ||
-            src_bvtype == bvtypet::IS_C_ENUM)
+            (src_bvtype == bvtypet::IS_C_ENUM && src_type.id() == ID_c_enum &&
+             to_c_enum_type(src_type).underlying_type().id() != ID_unsignedbv))
             l = src[src_width - 1]; // sign extension
           else
             l = const_literal(false); // zero extension
@@ -381,7 +395,9 @@ bool boolbvt::type_conversion(
       // destination type.
       // E.g., ((short)(ulong)(short)-1)==-1
       bool sign_extension =
-        src_bvtype == bvtypet::IS_SIGNED || src_bvtype == bvtypet::IS_C_ENUM;
+        src_bvtype == bvtypet::IS_SIGNED ||
+        (src_bvtype == bvtypet::IS_C_ENUM && src_type.id() == ID_c_enum &&
+         to_c_enum_type(src_type).underlying_type().id() != ID_unsignedbv);
 
       for(std::size_t i = 0; i < dest_width; i++)
       {