QF_Equality_LinearArith (Single Query Track)

Competition results for the QF_Equality_LinearArith division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_ALIA : 176 benchmarks
QF_AUFLIA : 505 benchmarks
QF_UFDTLIA : 76 benchmarks
QF_UFDTLIRA : 9 benchmarks
QF_UFIDL : 300 benchmarks
QF_UFLIA : 300 benchmarks
QF_UFLRA : 508 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
SMTInterpol	SMTInterpol	SMTInterpol	OpenSMT	SMTInterpol

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	0	1775 (base +0)	24298.77	24518.18	1775	976	799	99	0	99
SMTInterpol	0	1746	26026.56	18932.95	1747	995	752	127	0	88
cvc5	0	1735	41006.55	41225.24	1735	967	768	139	0	139
OpenSMT	0	1728	31073.46	31290.38	1728	939	789	61	85	61
Yices2	0	1702	26451.21	26664.48	1702	919	783	87	85	87
cvc5-cvc5-xyz ^ne	0	1702 (base -32)	33596.81	33808.42	1702	966	736	172	0	172
OpenSMT-SMTS-seq ^ne	4	1726 (base -2)	31566.74	31105.55	1730	944	786	59	85	59
z3-BooledASS-base ⁿ	0	1775	24402.91	24624.06	1775	976	799	99	0	99
cvc5-cvc5-xyz-base ⁿ	0	1734	40336.83	40555.58	1734	967	767	140	0	140
OpenSMT-SMTS-seq-base ⁿ	0	1728	31048.79	31266.51	1728	939	789	61	85	61

(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	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	0	1775 (base +0)	24298.77	24518.18	1775	976	799	99	0	99
SMTInterpol	0	1747	27390.91	20088.68	1747	995	752	127	0	88
cvc5	0	1735	41006.55	41225.24	1735	967	768	139	0	139
OpenSMT	0	1728	31073.46	31290.38	1728	939	789	61	85	61
Yices2	0	1702	26451.21	26664.48	1702	919	783	87	85	87
cvc5-cvc5-xyz ^ne	0	1702 (base -32)	33596.81	33808.42	1702	966	736	172	0	172
OpenSMT-SMTS-seq ^ne	4	1726 (base -2)	31566.74	31105.55	1730	944	786	59	85	59
z3-BooledASS-base ⁿ	0	1775	24402.91	24624.06	1775	976	799	99	0	99
cvc5-cvc5-xyz-base ⁿ	0	1734	40336.83	40555.58	1734	967	767	140	0	140
OpenSMT-SMTS-seq-base ⁿ	0	1728	31048.79	31266.51	1728	939	789	61	85	61

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
SMTInterpol	995	16740.64	12883.44	995	995	36	843	32
z3-BooledASS ^ne	976 (base +0)	13712.92	13833.41	976	976	55	843	55
cvc5	967	23110.50	23232.48	967	967	64	843	64
cvc5-cvc5-xyz ^ne	966 (base -1)	22565.87	22686.24	966	966	65	843	65
OpenSMT-SMTS-seq ^ne	940 (base +1)	12610.45	12459.62	940	940	31	903	31
OpenSMT	939	12636.63	12754.16	939	939	32	903	32
Yices2	919	13072.97	13188.05	919	919	52	903	52
z3-BooledASS-base ⁿ	976	13758.91	13880.65	976	976	55	843	55
cvc5-cvc5-xyz-base ⁿ	967	24438.29	24560.05	967	967	64	843	64
OpenSMT-SMTS-seq-base ⁿ	939	12421.89	12539.76	939	939	32	903	32

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	0	799 (base +0)	10585.84	10684.77	799	0	799	30	1045	30
OpenSMT	0	789	18436.83	18536.22	789	0	789	23	1062	23
Yices2	0	783	13378.24	13476.43	783	0	783	29	1062	29
cvc5	0	768	17896.06	17992.76	768	0	768	61	1045	61
SMTInterpol	0	752	10650.27	7205.23	752	0	752	77	1045	42
cvc5-cvc5-xyz ^ne	0	736 (base -31)	11030.93	11122.18	736	0	736	93	1045	93
OpenSMT-SMTS-seq ^ne	4	786 (base -3)	18956.29	18645.93	790	4	786	22	1062	22
z3-BooledASS-base ⁿ	0	799	10644.01	10743.41	799	0	799	30	1045	30
OpenSMT-SMTS-seq-base ⁿ	0	789	18626.90	18726.76	789	0	789	23	1062	23
cvc5-cvc5-xyz-base ⁿ	0	767	15898.55	15995.52	767	0	767	62	1045	62

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
z3-BooledASS ^ne	0	1694 (base +0)	1259.97	1467.44	1694	936	758	180
SMTInterpol	0	1662	7222.77	3139.40	1662	942	720	212
Yices2	0	1646	552.96	756.95	1646	889	757	228
cvc5	0	1597	1477.61	1675.31	1597	885	712	277
OpenSMT	0	1593	1971.97	2168.89	1593	868	725	281
cvc5-cvc5-xyz ^ne	0	1570 (base -25)	1628.70	1821.09	1570	879	691	304
OpenSMT-SMTS-seq ^ne	4	1581 (base -10)	2094.40	2253.27	1585	867	718	289
z3-BooledASS-base ⁿ	0	1694	1263.65	1472.84	1694	936	758	180
cvc5-cvc5-xyz-base ⁿ	0	1595	1507.32	1704.82	1595	883	712	279
OpenSMT-SMTS-seq-base ⁿ	0	1591	1926.36	2123.67	1591	866	725	283

SMT-COMP 2026