diff --git a/cpp/impl.cpp b/cpp/impl.cpp
index 31d8267c..0c39a799 100644
--- a/cpp/impl.cpp
+++ b/cpp/impl.cpp
@@ -1891,8 +1891,20 @@ class PALConsumer : public ASTConsumer {
 
       // Evaluate scrutinee
       auto scrutRval = trRValue(sw->getCond());
-      auto scrutTy =
-          trQualType(sw->getCond()->getType(), sw->getCond()->getSourceRange());
+      // Clang applies the integral promotions to the switch condition. An
+      // enumeration is modeled by its underlying integer type, so that
+      // promotion translates to the identity and is elided from the rvalue.
+      // Annotating the binding with the promoted type would then leave the
+      // declared type and the translated value syntactically distinct, which
+      // the Pulse dereference tactic rejects. Use the enumeration's own type
+      // so the two agree; other promotions are genuine casts that trRValue
+      // preserves, so their promoted type remains correct.
+      auto *scrutExpr = sw->getCond();
+      auto scrutQualTy = scrutExpr->getType();
+      if (scrutExpr->IgnoreImpCasts()->getType()->isEnumeralType()) {
+        scrutQualTy = scrutExpr->IgnoreImpCasts()->getType();
+      }
+      auto scrutTy = trQualType(scrutQualTy, scrutExpr->getSourceRange());
 
       // Bind the scrutinee once as an immutable value.
       static int switchCounter = 0;
diff --git a/src/pass/prune.rs b/src/pass/prune.rs
index 07b27dad..4a151207 100644
--- a/src/pass/prune.rs
+++ b/src/pass/prune.rs
@@ -154,7 +154,12 @@ fn scan_inline_pulse_code(deps: &mut HashSet<DeclName>, code: &InlinePulseCode)
 
 fn scan_expr(deps: &mut HashSet<DeclName>, rv: &Expr) {
     match &rv.val {
-        ExprT::Var(_) => {}
+        // A bare name may refer to a global (an enum constant, say). Locals share the namespace,
+        // so this over-approximates -- which is the safe direction for a pruner: it can keep a
+        // declaration that is not needed, but must never drop one that is.
+        ExprT::Var(n) => {
+            deps.insert(DeclName::GlobalVar(n.val.clone()));
+        }
         ExprT::Deref(v) => scan_expr(deps, v),
         ExprT::Member(x, _a) => scan_expr(deps, x),
         ExprT::VAttr(_, x) => scan_expr(deps, x),
diff --git a/test/enum_const_in_contract/Makefile b/test/enum_const_in_contract/Makefile
new file mode 120000
index 00000000..3febeb16
--- /dev/null
+++ b/test/enum_const_in_contract/Makefile
@@ -0,0 +1 @@
+../_templates/Makefile
\ No newline at end of file
diff --git a/test/enum_const_in_contract/colors.h b/test/enum_const_in_contract/colors.h
new file mode 100644
index 00000000..d0db032f
--- /dev/null
+++ b/test/enum_const_in_contract/colors.h
@@ -0,0 +1,20 @@
+#pragma once
+#include "pal.h"
+
+// These enumerators live in a header, so the pruner sees them as non-root
+// declarations. The contract below is their only reference: the body uses a
+// switch, whose case labels the C frontend folds to integer constants.
+typedef enum _COLOR
+{
+    Color_Red = 0,
+    Color_Green = 1,
+    Color_Blue = 2,
+} COLOR;
+
+_Bool
+color_is_known(COLOR c)
+    _ensures(return == (c == Color_Red || c == Color_Green || c == Color_Blue));
+
+COLOR
+color_default(void)
+    _ensures(return == Color_Green);
diff --git a/test/enum_const_in_contract/enum_const_in_contract.c b/test/enum_const_in_contract/enum_const_in_contract.c
new file mode 100644
index 00000000..af82701c
--- /dev/null
+++ b/test/enum_const_in_contract/enum_const_in_contract.c
@@ -0,0 +1,26 @@
+#include "colors.h"
+
+_Bool
+color_is_known(COLOR c)
+{
+    _Bool known = 0;
+
+    switch (c)
+    {
+    case Color_Red:
+    case Color_Green:
+    case Color_Blue:
+        known = 1;
+        break;
+    default:
+        break;
+    }
+
+    return known;
+}
+
+COLOR
+color_default(void)
+{
+    return Color_Green;
+}
diff --git a/test/enum_const_in_contract/fstar.fst.config.json b/test/enum_const_in_contract/fstar.fst.config.json
new file mode 120000
index 00000000..4100b019
--- /dev/null
+++ b/test/enum_const_in_contract/fstar.fst.config.json
@@ -0,0 +1 @@
+../_templates/fstar.fst.config.json
\ No newline at end of file
diff --git a/test/enum_const_in_contract/pal.config.json b/test/enum_const_in_contract/pal.config.json
new file mode 120000
index 00000000..d59f1cfa
--- /dev/null
+++ b/test/enum_const_in_contract/pal.config.json
@@ -0,0 +1 @@
+../_templates/pal.config.json
\ No newline at end of file
diff --git a/test/enum_const_in_contract/pal.h b/test/enum_const_in_contract/pal.h
new file mode 120000
index 00000000..05ef83f9
--- /dev/null
+++ b/test/enum_const_in_contract/pal.h
@@ -0,0 +1 @@
+../pal.h
\ No newline at end of file