Equality_LinearArith (Unsat Core Track)

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

Results were generated on 2026-07-25

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

Logics:

ALIA : 154 benchmarks
AUFDTLIA : 186 benchmarks
AUFDTLIRA : 1385 benchmarks
AUFLIA : 649 benchmarks
AUFLIRA : 2377 benchmarks
UFDTLIA : 532 benchmarks
UFDTLIRA : 972 benchmarks
UFIDL : 30 benchmarks
UFLIA : 1172 benchmarks
UFLRA : 10 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	811923	33034.89	33953.80	7359	7359	108	0	79
z3-BooledASS ^ne	782155 (base +2006)	9159.57	10031.48	7076	7076	391	0	186
SMTInterpol	409286	48168.33	35651.42	6112	6112	1355	0	1121
UltimateEliminator+MathSAT	2816	961.15	518.19	146	146	4246	3075	1
z3-BooledASS-base ⁿ	780149	6557.17	7428.91	7076	7076	391	0	254

(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	811923	33034.89	33953.80	7359	7359	108	0	79
z3-BooledASS ^ne	782155 (base +2006)	9159.57	10031.48	7076	7076	391	0	186
SMTInterpol	409959	54743.99	38964.87	6112	6112	1355	0	1121
UltimateEliminator+MathSAT	2816	961.15	518.19	146	146	4246	3075	1
z3-BooledASS-base ⁿ	780149	6557.17	7428.91	7076	7076	391	0	254

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	811923	33034.89	33953.80	7359	7359	108	0	79
z3-BooledASS ^ne	782155 (base +2006)	9159.57	10031.48	7076	7076	391	0	186
SMTInterpol	409959	54743.99	38964.87	6112	6112	1355	0	1121
UltimateEliminator+MathSAT	2816	961.15	518.19	146	146	4246	3075	1
z3-BooledASS-base ⁿ	780149	6557.17	7428.91	7076	7076	391	0	254

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
cvc5	785637	2595.37	3494.53	7221	7221	19	227
z3-BooledASS ^ne	778536 (base +1441)	1754.34	2622.64	7055	7055	180	232
SMTInterpol	396797	13561.23	6885.90	5960	5960	24	1483
UltimateEliminator+MathSAT	2227	768.39	335.53	145	145	4240	3082
z3-BooledASS-base ⁿ	777095	1768.26	2637.09	7057	7057	103	307

SMT-COMP 2026