diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
index 7a3c0231e815..33eca49ba6a5 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
@@ -343,7 +343,7 @@ where
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return none
+    let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← ofAtom x
     let bvExpr : BVExpr width := .const bvVal
     let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr width) (toExpr bvVal)
     let proof := do
diff --git a/tests/lean/run/bv_decide_nat.lean b/tests/lean/run/bv_decide_nat.lean
new file mode 100644
index 000000000000..3b5634d3137f
--- /dev/null
+++ b/tests/lean/run/bv_decide_nat.lean
@@ -0,0 +1,4 @@
+import Std.Tactic.BVDecide
+
+theorem cex (n : Nat) (hn : BitVec.ofNat 64 n ≠ 0) : BitVec.ofNat 64 n ≠ 0#64 := by
+  bv_decide