perf: benchmark for modulo on bv_decide

[hargoniX]

This verifies a bit hack from here: https://en.wikipedia.org/wiki/Lehmer_random_number_generator#Sample_C99_code

I previously ran the SMTLIB equivalent this with Bitwuzla in my crypto class and got the following numbers:

• 22s with Bitwuzla
• Z3 and CVC5 don't yet terminate after > 2min

Now withbv_decide the overall timing is 33.7s, consisting of:

• 5s of checking the LRAT cert
• 5s of trimming the LRAT cert from 800k to 300k proof steps
• remainder actual solving time

So running bv_decide like a normal SMT solver without verifying the result of the SAT solver would yield approximately ~24s.

[hargoniX]

!bench

[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 abae95e1701a081701ef132a35b3b409594e3907 --onto 3e75d8f74297bc258352f8d89f71496aacefe7ae. (2024-10-08 15:17:49)

[leanprover-bot]

Here are the benchmark results for commit b2366db.
There were significant changes against commit abae95e:

  Benchmark             Metric   Change
  ================================================
+ bv_decide_realworld   maxrss    -1.2% (-225.1 σ)

[tobiasgrosser]

Nice.