From ac8e46f7b0396cfe3434713fb0ad7c04e0f7a44b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 26 Sep 2024 23:21:01 +0200 Subject: [PATCH] fix: handling BitVec.ofNat with Nat fvars in bv_decide As reported by @bollu. --- .../Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean | 2 +- tests/lean/run/bv_decide_nat.lean | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/bv_decide_nat.lean 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