bd091f119b
This example, reported from LNSym, started failing when we changed the definition of `Fin.sub` in https://github.com/leanprover/lean4/pull/4421. When we use the new definition, `omega` produces a proof term that the kernel is very slow on. To work around this for now, I've removed `BitVec.toNat_sub` from the `bv_toNat` simp set, and replaced it with `BitVec.toNat_sub'` which uses the old definition for subtraction. This is only a workaround, and I would like to understand why the term chokes the kernel. ``` example (n : Nat) (addr2 addr1 : BitVec 64) (h0 : n ≤ 18446744073709551616) (h1 : addr2 + 18446744073709551615#64 - addr1 ≤ BitVec.ofNat 64 (n - 1)) (h2 : addr2 - addr1 ≤ addr2 + 18446744073709551615#64 - addr1) : n = 18446744073709551616 := by bv_omega ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||