QF_UFLRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Yices2	507	1155.88	1218.98	507	282	225	1	1
cvc5-cvc5-xyz ^ne	506 (base +0)	451.94	513.72	506	281	225	2	2
cvc5	506	543.11	605.38	506	281	225	2	2
OpenSMT-SMTS-seq	505 (base +1)	1129.95	1178.65	505	280	225	3	3
SMTInterpol	505	3334.77	1344.88	506	282	224	2	1
OpenSMT	505	2434.80	2497.38	505	280	225	3	3
z3-BooledASS ^ne	501 (base +0)	1373.74	1435.16	501	278	223	7	7
cvc5-cvc5-xyz-base ⁿ	506	555.44	617.81	506	281	225	2	2
OpenSMT-SMTS-seq-base ⁿ	504	1256.34	1318.90	504	279	225	4	4
z3-BooledASS-base ⁿ	501	1368.45	1430.39	501	278	223	7	7

(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
Yices2	507	1155.88	1218.98	507	282	225	1	1
cvc5-cvc5-xyz ^ne	506 (base +0)	451.94	513.72	506	281	225	2	2
cvc5	506	543.11	605.38	506	281	225	2	2
SMTInterpol	506	4699.13	2500.61	506	282	224	2	1
OpenSMT-SMTS-seq	505 (base +1)	1129.95	1178.65	505	280	225	3	3
OpenSMT	505	2434.80	2497.38	505	280	225	3	3
z3-BooledASS ^ne	501 (base +0)	1373.74	1435.16	501	278	223	7	7
cvc5-cvc5-xyz-base ⁿ	506	555.44	617.81	506	281	225	2	2
OpenSMT-SMTS-seq-base ⁿ	504	1256.34	1318.90	504	279	225	4	4
z3-BooledASS-base ⁿ	501	1368.45	1430.39	501	278	223	7	7

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Yices2	282	1113.99	1149.09	282	282	1	225	1
SMTInterpol	282	3265.76	1908.45	282	282	1	225	1
cvc5-cvc5-xyz ^ne	281 (base +0)	267.63	301.86	281	281	2	225	2
cvc5	281	385.37	420.06	281	281	2	225	2
OpenSMT-SMTS-seq	280 (base +1)	1020.00	1036.57	280	280	3	225	3
OpenSMT	280	2347.46	2382.23	280	280	3	225	3
z3-BooledASS ^ne	278 (base +0)	812.91	846.94	278	278	5	225	5
cvc5-cvc5-xyz-base ⁿ	281	398.78	433.34	281	281	2	225	2
OpenSMT-SMTS-seq-base ⁿ	279	1165.78	1200.43	279	279	4	225	4
z3-BooledASS-base ⁿ	278	808.49	842.94	278	278	5	225	5

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Yices2	225	41.88	69.88	225	225	0	283	0
OpenSMT	225	87.35	115.14	225	225	0	283	0
OpenSMT-SMTS-seq ^ne	225 (base +0)	109.94	142.08	225	225	0	283	0
cvc5	225	157.74	185.33	225	225	0	283	0
cvc5-cvc5-xyz ^ne	225 (base +0)	184.32	211.85	225	225	0	283	0
SMTInterpol	224	1433.36	592.16	224	224	1	283	0
z3-BooledASS ^ne	223 (base +0)	560.82	588.22	223	223	2	283	2
OpenSMT-SMTS-seq-base ⁿ	225	90.56	118.47	225	225	0	283	0
cvc5-cvc5-xyz-base ⁿ	225	156.66	184.47	225	225	0	283	0
z3-BooledASS-base ⁿ	223	559.96	587.45	223	223	2	283	2

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
Yices2	506	101.69	164.58	506	281	225	2
cvc5-cvc5-xyz ^ne	501 (base +1)	219.31	280.45	501	277	224	7
cvc5	500	147.03	208.53	500	277	223	8
SMTInterpol	499	1840.62	729.34	499	277	222	9
OpenSMT-SMTS-seq ^ne	495 (base +4)	417.99	478.48	495	270	225	13
z3-BooledASS ^ne	494 (base +0)	219.15	279.69	494	276	218	14
OpenSMT	491	319.14	379.79	491	266	225	17
cvc5-cvc5-xyz-base ⁿ	500	151.88	213.47	500	277	223	8
z3-BooledASS-base ⁿ	494	219.01	280.03	494	276	218	14
OpenSMT-SMTS-seq-base ⁿ	491	300.75	361.57	491	266	225	17

SMT-COMP 2026