diff --git a/regression/cbmc/enum_unsigned_widen/main.c b/regression/cbmc/enum_unsigned_widen/main.c
new file mode 100644
index 00000000000..937df433a5c
--- /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 00000000000..749292d9497
--- /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 64c82b1e0ac..2301c668027 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++)
       {