feat: bv_decide inequality regression tests

[alexkeizer]

This takes a few standalone bitvector problems, about inequalties, from LNSym, and adds them as a benchmark to prevent further regressions with bv_decide.

These problems are particularly interesting, because they've previously had a bad interaction with bv_decides normalization pass, see #5664.

[hargoniX]

!bench to get a baseline with ac_nf enabled

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3d175ab25fb0f548be3b5d29f376ed8e32f10137 --onto 225e08965d644715e8961cd205ffedf1cf7d24c2. (2024-10-14 21:42:44)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase adfbc56f9100257da410e9c36f6f90ca203b6eeb --onto 225e08965d644715e8961cd205ffedf1cf7d24c2. (2024-10-14 22:12:04)
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-10-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-10-15 08:54:25)

[leanprover-bot]

Here are the benchmark results for commit 59413c1.
There were significant changes against commit 3d175ab:

  Benchmark            Metric       Change
  ==================================================
- import Lean          task-clock     8.3%  (60.2 σ)
- import Lean          wall-clock     8.3%  (71.8 σ)
+ lake build clean     wall-clock    -1.4% (-11.0 σ)
- lake config import   task-clock     8.2%  (11.7 σ)
- lake config import   wall-clock     8.2%  (10.9 σ)
- unionfind            task-clock     6.6%  (16.3 σ)
- unionfind            wall-clock     6.6%  (16.1 σ)

[hargoniX]

!bench and now without ac_nf

[alexkeizer]

Note that the worst offender has the normalization pass explicitly disabled (because it times out otherwise), so the baseline will be somewhat skewed

[leanprover-bot]

Here are the benchmark results for commit 16acc72.Found no runs to compare against.