fix: handling BitVec.ofNat with Nat fvars in bv_decide (#5484)

leanprover · Sep 26, 2024 · 13969ad · 13969ad
1 parent 91a0334
commit 13969ad
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git 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
@@ -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