diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
index 581b79cff4..ce60b7560e 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -47,9 +47,11 @@ where
       binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr origExpr
     | Complement.complement _ _ innerExpr =>
       unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr origExpr
-    | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
+    | HShiftLeft.hShiftLeft α β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
-      if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
+      let_expr BitVec wExpr := α | return none
+      if (← getNatValue? wExpr).isSome && distance?.isSome then
+        throwError "internal error: constant shift should have been eliminated."
       let_expr BitVec _ := β | return none
       shiftReflection
         distanceExpr
@@ -58,9 +60,11 @@ where
         ``BVExpr.shiftLeft
         ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
         origExpr
-    | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
+    | HShiftRight.hShiftRight α β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
-      if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
+      let_expr BitVec wExpr := α | return none
+      if (← getNatValue? wExpr).isSome && distance?.isSome then
+        throwError "internal error: constant shift should have been eliminated."
       let_expr BitVec _ := β | return none
       shiftReflection
         distanceExpr
diff --git a/tests/lean/run/bv_decide_shift_error.lean b/tests/lean/run/bv_decide_shift_error.lean
new file mode 100644
index 0000000000..aa20fb0f92
--- /dev/null
+++ b/tests/lean/run/bv_decide_shift_error.lean
@@ -0,0 +1,14 @@
+import Std.Tactic.BVDecide
+
+-- This previously was an internal error due to the constant shift not being eliminated because
+-- of the non constant width shift, now it's an error.
+
+/--
+error: The prover found a potentially spurious counterexample:
+- It abstracted the following unsupported expressions as opaque variables: [x <<< 1 == x]
+Consider the following assignment:
+x <<< 1 == x = false
+-/
+#guard_msgs in
+example (x : BitVec w) : x <<< (1 : Nat) = x := by
+  bv_decide