Equality_MachineArith (Unsat Core Track)

Competition results for the Equality_MachineArith division in the Unsat Core Track. Chart

Results were generated on 2026-07-25

Benchmarks: 2781
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Logics:

ABV : 193 benchmarks
ABVFP : 3 benchmarks
ABVFPLRA : 4 benchmarks
AUFBV : 1 benchmarks
AUFBVDTLIA : 153 benchmarks
AUFBVDTNIA : 300 benchmarks
AUFBVDTNIRA : 879 benchmarks
AUFBVFPDTNIRA : 60 benchmarks
AUFFPDTNIRA : 132 benchmarks
UFBVDTLIA : 24 benchmarks
UFBVDTNIA : 157 benchmarks
UFBVDTNIRA : 500 benchmarks
UFBVFPDTNIRA : 75 benchmarks
UFFPDTNIRA : 300 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	-	cvc5	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	167957	40956.65	41253.76	2371	2371	410	0	397
SMTInterpol	109180	24078.81	18365.40	1492	1492	715	574	541
z3-BooledASS ^ne	62979 (base -97292)	1448.26	1491.54	351	351	2430	0	918
Bitwuzla	154	1746.98	1754.09	54	54	147	2580	147
Bitwuzla-fixed ⁿ	0	0.00	0.00	0	0	201	2580	0
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	201	2580	0
z3-BooledASS-base ⁿ	160271	12803.56	13065.30	2115	2115	666	0	363

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	167957	40956.65	41253.76	2371	2371	410	0	397
SMTInterpol	109180	24078.81	18365.40	1492	1492	715	574	541
z3-BooledASS ^ne	62979 (base -97292)	1448.26	1491.54	351	351	2430	0	918
Bitwuzla	154	1746.98	1754.09	54	54	147	2580	147
Bitwuzla-fixed ⁿ	0	0.00	0.00	0	0	201	2580	0
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	201	2580	0
z3-BooledASS-base ⁿ	160271	12803.56	13065.30	2115	2115	666	0	363

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	167957	40956.65	41253.76	2371	2371	410	0	397
SMTInterpol	109180	24078.81	18365.40	1492	1492	715	574	541
z3-BooledASS ^ne	62979 (base -97292)	1448.26	1491.54	351	351	2430	0	918
Bitwuzla	154	1746.98	1754.09	54	54	147	2580	147
Bitwuzla-fixed ⁿ	0	0.00	0.00	0	0	201	2580	0
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	201	2580	0
z3-BooledASS-base ⁿ	160271	12803.56	13065.30	2115	2115	666	0	363

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
cvc5	166148	834.15	1102.73	2176	2176	9	596
SMTInterpol	100651	5495.85	2269.90	1407	1407	69	1305
z3-BooledASS ^ne	62810 (base -95647)	170.39	212.89	346	346	1475	960
Bitwuzla	125	43.51	49.19	46	46	0	2735
Bitwuzla-fixed ⁿ	0	0.00	0.00	0	0	201	2580
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	201	2580
z3-BooledASS-base ⁿ	158457	1027.23	1280.66	2059	2059	214	508

SMT-COMP 2026