QF_UFLIA (Single Query Track)

Competition results for the QF_UFLIA logic in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
SMTInterpol	291	5632.29	4562.53	291	218	73	9	9
z3-BooledASS ^ne	289 (base +0)	555.81	591.30	289	217	72	11	11
Yices2	289	2539.01	2575.09	289	217	72	11	11
cvc5	285	3148.90	3184.60	285	216	69	15	15
OpenSMT	282	2517.93	2552.97	282	212	70	18	18
OpenSMT-SMTS-seq ^ne	281 (base -1)	1722.32	1721.67	281	211	70	19	19
cvc5-cvc5-xyz ^ne	271 (base -14)	7961.36	7995.38	271	202	69	29	29
z3-BooledASS-base ⁿ	289	557.83	593.49	289	217	72	11	11
cvc5-cvc5-xyz-base ⁿ	285	3530.00	3565.48	285	216	69	15	15
OpenSMT-SMTS-seq-base ⁿ	282	2539.48	2574.77	282	212	70	18	18

(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	Timeout
SMTInterpol	291	5632.29	4562.53	291	218	73	9	9
z3-BooledASS ^ne	289 (base +0)	555.81	591.30	289	217	72	11	11
Yices2	289	2539.01	2575.09	289	217	72	11	11
cvc5	285	3148.90	3184.60	285	216	69	15	15
OpenSMT	282	2517.93	2552.97	282	212	70	18	18
OpenSMT-SMTS-seq ^ne	281 (base -1)	1722.32	1721.67	281	211	70	19	19
cvc5-cvc5-xyz ^ne	271 (base -14)	7961.36	7995.38	271	202	69	29	29
z3-BooledASS-base ⁿ	289	557.83	593.49	289	217	72	11	11
cvc5-cvc5-xyz-base ⁿ	285	3530.00	3565.48	285	216	69	15	15
OpenSMT-SMTS-seq-base ⁿ	282	2539.48	2574.77	282	212	70	18	18

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
SMTInterpol	218	3163.64	2467.64	218	218	4	78	4
z3-BooledASS ^ne	217 (base +0)	328.50	355.15	217	217	5	78	5
Yices2	217	2090.36	2117.51	217	217	5	78	5
cvc5	216	3024.28	3051.47	216	216	6	78	6
OpenSMT	212	2442.62	2469.04	212	212	10	78	10
OpenSMT-SMTS-seq ^ne	211 (base -1)	1624.99	1616.08	211	211	11	78	11
cvc5-cvc5-xyz ^ne	202 (base -14)	6971.74	6997.19	202	202	20	78	20
z3-BooledASS-base ⁿ	217	329.35	356.19	217	217	5	78	5
cvc5-cvc5-xyz-base ⁿ	216	3391.33	3418.27	216	216	6	78	6
OpenSMT-SMTS-seq-base ⁿ	212	2464.51	2491.15	212	212	10	78	10

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
SMTInterpol	73	2468.65	2094.88	73	73	1	226	1
z3-BooledASS ^ne	72 (base +0)	227.30	236.15	72	72	2	226	2
Yices2	72	448.64	457.58	72	72	2	226	2
OpenSMT	70	75.30	83.93	70	70	4	226	4
OpenSMT-SMTS-seq ^ne	70 (base +0)	97.33	105.59	70	70	4	226	4
cvc5	69	124.62	133.14	69	69	5	226	5
cvc5-cvc5-xyz ^ne	69 (base +0)	989.62	998.19	69	69	5	226	5
z3-BooledASS-base ⁿ	72	228.48	237.29	72	72	2	226	2
OpenSMT-SMTS-seq-base ⁿ	70	74.97	83.62	70	70	4	226	4
cvc5-cvc5-xyz-base ⁿ	69	138.66	147.20	69	69	5	226	5

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
z3-BooledASS ^ne	283 (base +0)	198.12	232.88	283	213	70	17
Yices2	281	184.11	218.97	281	210	71	19
OpenSMT	273	441.54	475.16	273	204	69	27
cvc5	271	205.76	239.39	271	205	66	29
SMTInterpol	271	947.28	420.98	271	204	67	29
OpenSMT-SMTS-seq ^ne	270 (base -3)	443.83	467.44	270	201	69	30
cvc5-cvc5-xyz ^ne	249 (base -21)	345.31	375.85	249	183	66	51
z3-BooledASS-base ⁿ	283	195.55	230.46	283	213	70	17
OpenSMT-SMTS-seq-base ⁿ	273	441.48	475.31	273	204	69	27
cvc5-cvc5-xyz-base ⁿ	270	198.34	231.60	270	204	66	30

SMT-COMP 2026