test: increase split budget in `grind_bitvec2` bench The `replicate_append_self` goal needs the exponent identity `w + w * n = w * (n + 1)` to relate `2 ^ _` terms in the `toNat` images of the appends. `grind` finds it only via a model-based theory combination case split, and the homomorphism encoding eagerly translates every `BitVec` term (including `cast` variants), producing enough competing exponent-pair split candidates that the default budget of 9 is no longer sufficient; the goal needs 11. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.