chore: run small width independent test evaluation in CI

[bollu]

This allows us to make sure that our width independent code runs correctly, which will help with the larger refactor in mind of the test pipeline

[github-actions]

Alive Statistics: 90 / 93 (3 failed)

[github-actions]

bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gexact_proof
bitwuzla proved and bv_decide failed theorem 14 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 19 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 40 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 51 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 53 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdivhshift_proof
bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdistribute_proof
bitwuzla proved and bv_decide failed theorem 4 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gdistribute_proof
bitwuzla proved and bv_decide failed theorem 12 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gnarrowhmath_proof
bitwuzla proved and bv_decide failed theorem 9 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gapinthsub_proof
bitwuzla proved and bv_decide failed theorem 1 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gapinthrem2_proof
bitwuzla proved and bv_decide failed theorem 17 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/grem_proof
bitwuzla proved and bv_decide failed theorem 1 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd4_proof
bitwuzla proved and bv_decide failed theorem 3 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd4_proof
bitwuzla proved and bv_decide failed theorem 0 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2008h02h23hMulSub_proof
bitwuzla proved and bv_decide failed theorem 0 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2010h11h23hDistributed_proof
bitwuzla proved and bv_decide failed theorem 4 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd_or_sub_proof
bitwuzla proved and bv_decide failed theorem 15 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gshifthshift_proof
bitwuzla proved and bv_decide failed theorem 7 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gtrunchinseltpoison_proof
bitwuzla proved and bv_decide failed theorem 14 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gshlhfactor_proof
bitwuzla proved and bv_decide failed theorem 21 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 22 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 23 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 24 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/greassociatehnuw_proof
bitwuzla proved and bv_decide failed theorem 6 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gadd2_proof
bitwuzla proved and bv_decide failed theorem 5 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/g2012h08h28hudiv_ashl_proof
bitwuzla proved and bv_decide failed theorem 13 in file /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/results/InstCombine/gsubhxorhcmp_proof
bv_decide solved 7814 theorems.
bitwuzla solved 7841 theorems.
bv_decide found 0 counterexamples.
bitwuzla found 0 counterexamples.
bv_decide only failed on 27 problems.
bitwuzla only failed on 0 problems.
both bitwuzla and bv_decide failed on 27 problems.
In total, bitwuzla saw 7868 problems.
In total, bv_decide saw 7868 problems.
ran rg 'LeanSAT provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'Bitwuzla provided a counter' | wc -l, this file found 0, rg found 0, SUCCESS
ran rg 'LeanSAT proved' | wc -l, this file found 7814, rg found 0, FAIL
ran rg 'Bitwuzla proved' | wc -l, this file found 7841, rg found 0, FAIL
The InstCombine benchmark contains 4520 theorems in total.
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_ceg_data.csv
all_files_solved_bitwuzla_times_stddev avg: 212.055435 | stddev: 0.0
all_files_solved_bv_decide_times_stddev avg: 250.64963749999998 | stddev: 0.0
all_files_solved_bv_decide_rw_times_stddev avg: 102.553402 | stddev: 0.0
all_files_solved_bv_decide_bb_times_stddev avg: 0.096511 | stddev: 0.0
all_files_solved_bv_decide_sat_times_stddev avg: 91.2670095 | stddev: 0.0
all_files_solved_bv_decide_lratt_times_stddev avg: 0.12331349999999999 | stddev: 0.0
all_files_solved_bv_decide_lratc_times_stddev avg: 27.143984 | stddev: 0.0
mean of percentage stddev/av: 0.0%
max of percentage stddev/av: 0.0%
Saved dataframe at: /home/ubuntu/_work/lean-mlir/lean-mlir/bv-evaluation/raw-data/InstCombine/instcombine_solved_data.csv