Equality_NonLinearArith (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

ANIA : 78 benchmarks
AUFDTNIRA : 545 benchmarks
AUFNIA : 3 benchmarks
AUFNIRA : 300 benchmarks
UFDTNIA : 500 benchmarks
UFDTNIRA : 806 benchmarks
UFNIA : 1662 benchmarks
UFNIRA : 258 benchmarks

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	2778	57869.95	58222.72	2778	195	2583	1374	0	1065
cvc5-cvc5-xyz ^ne	2777 (base +0)	58438.45	58786.29	2777	195	2582	1375	0	1066
z3-BooledASS ^ne	2673 (base -5)	5638.73	5967.86	2673	240	2433	1479	0	1372
SMTInterpol	1255	14078.77	10268.20	1255	21	1234	2897	0	1473
UltimateEliminator+MathSAT	189	1516.27	1081.54	189	135	54	2112	1851	107
cvc5-cvc5-xyz-base ⁿ	2777	57970.53	58318.70	2777	195	2582	1375	0	1066
z3-BooledASS-base ⁿ	2678	7356.53	7685.34	2678	241	2437	1474	0	1231

(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 SAT	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	2778	57869.95	58222.72	2778	195	2583	1374	0	1065
cvc5-cvc5-xyz ^ne	2777 (base +0)	58438.45	58786.29	2777	195	2582	1375	0	1066
z3-BooledASS ^ne	2673 (base -5)	5638.73	5967.86	2673	240	2433	1479	0	1372
SMTInterpol	1255	14078.77	10268.20	1255	21	1234	2897	0	1473
UltimateEliminator+MathSAT	189	1516.27	1081.54	189	135	54	2112	1851	107
cvc5-cvc5-xyz-base ⁿ	2777	57970.53	58318.70	2777	195	2582	1375	0	1066
z3-BooledASS-base ⁿ	2678	7356.53	7685.34	2678	241	2437	1474	0	1231

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	240 (base -1)	73.35	102.98	240	240	68	3844	58
cvc5	195	8042.51	8067.51	195	195	113	3844	9
cvc5-cvc5-xyz ^ne	195 (base +0)	8051.69	8076.64	195	195	113	3844	9
UltimateEliminator+MathSAT	135	1274.49	966.65	135	135	163	3854	44
SMTInterpol	21	9.67	9.58	21	21	287	3844	56
z3-BooledASS-base ⁿ	241	75.36	105.00	241	241	67	3844	54
cvc5-cvc5-xyz-base ⁿ	195	8051.95	8076.81	195	195	113	3844	9

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	2583	49827.44	50155.21	2583	2583	228	1341	157
cvc5-cvc5-xyz ^ne	2582 (base +0)	50386.75	50709.65	2582	2582	229	1341	158
z3-BooledASS ^ne	2433 (base -4)	5565.37	5864.88	2433	2433	378	1341	331
SMTInterpol	1234	14069.10	10258.61	1234	1234	1577	1341	805
UltimateEliminator+MathSAT	54	241.78	114.89	54	54	1071	3027	43
cvc5-cvc5-xyz-base ⁿ	2582	49918.58	50241.89	2582	2582	229	1341	158
z3-BooledASS-base ⁿ	2437	7281.17	7580.33	2437	2437	374	1341	290

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	2637 (base +1)	1548.02	1872.36	2637	240	2397	76	1439
cvc5	2506	2922.67	3236.37	2506	178	2328	307	1339
cvc5-cvc5-xyz ^ne	2501 (base -1)	2943.40	3252.09	2501	178	2323	307	1344
SMTInterpol	1227	4649.29	2087.05	1227	21	1206	998	1927
UltimateEliminator+MathSAT	185	1089.33	665.01	185	131	54	1995	1972
z3-BooledASS-base ⁿ	2636	1480.99	1804.05	2636	241	2395	77	1439
cvc5-cvc5-xyz-base ⁿ	2502	2959.55	3268.56	2502	178	2324	307	1343

SMT-COMP 2026