QF_UFIDL (Single Query Track)

Competition results for the QF_UFIDL 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)
OpenSMT	OpenSMT	OpenSMT-SMTS-seq	OpenSMT	OpenSMT

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
OpenSMT-SMTS-seq ^ne	280 (base +2)	21071.89	20634.07	280	100	180	20	20
OpenSMT	278	21063.79	21100.54	278	99	179	22	22
z3-BooledASS ^ne	261 (base +0)	9886.27	9918.90	261	88	173	39	39
Yices2	239	20758.02	20789.45	239	68	171	61	61
cvc5	234	27249.31	27280.74	234	86	148	66	66
SMTInterpol	210	4154.91	2443.65	210	87	123	90	56
cvc5-cvc5-xyz ^ne	194 (base -40)	17025.35	17050.73	194	77	117	106	106
OpenSMT-SMTS-seq-base ⁿ	278	21273.70	21310.55	278	99	179	22	22
z3-BooledASS-base ⁿ	261	9942.56	9975.64	261	88	173	39	39
cvc5-cvc5-xyz-base ⁿ	234	26380.08	26411.67	234	87	147	66	66

(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
OpenSMT-SMTS-seq ^ne	280 (base +2)	21071.89	20634.07	280	100	180	20	20
OpenSMT	278	21063.79	21100.54	278	99	179	22	22
z3-BooledASS ^ne	261 (base +0)	9886.27	9918.90	261	88	173	39	39
Yices2	239	20758.02	20789.45	239	68	171	61	61
cvc5	234	27249.31	27280.74	234	86	148	66	66
SMTInterpol	210	4154.91	2443.65	210	87	123	90	56
cvc5-cvc5-xyz ^ne	194 (base -40)	17025.35	17050.73	194	77	117	106	106
OpenSMT-SMTS-seq-base ⁿ	278	21273.70	21310.55	278	99	179	22	22
z3-BooledASS-base ⁿ	261	9942.56	9975.64	261	88	173	39	39
cvc5-cvc5-xyz-base ⁿ	234	26380.08	26411.67	234	87	147	66	66

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
OpenSMT-SMTS-seq	100 (base +1)	4176.77	4089.53	100	100	2	198	2
OpenSMT	99	4145.37	4158.27	99	99	3	198	3
z3-BooledASS ^ne	88 (base +0)	364.19	374.77	88	88	14	198	14
SMTInterpol	87	1446.46	907.26	87	87	15	198	15
cvc5	86	12338.57	12350.32	86	86	16	198	16
cvc5-cvc5-xyz ^ne	77 (base -10)	8949.35	8959.68	77	77	25	198	25
Yices2	68	7927.43	7936.63	68	68	34	198	34
OpenSMT-SMTS-seq-base ⁿ	99	4191.08	4203.95	99	99	3	198	3
z3-BooledASS-base ⁿ	88	362.58	373.47	88	88	14	198	14
cvc5-cvc5-xyz-base ⁿ	87	13519.90	13531.98	87	87	15	198	15

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
OpenSMT-SMTS-seq ^ne	180 (base +1)	16895.12	16544.54	180	180	18	102	18
OpenSMT	179	16918.43	16942.27	179	179	19	102	19
z3-BooledASS ^ne	173 (base +0)	9522.07	9544.13	173	173	25	102	25
Yices2	171	12830.58	12852.82	171	171	27	102	27
cvc5	148	14910.74	14930.42	148	148	50	102	50
SMTInterpol	123	2708.46	1536.39	123	123	75	102	41
cvc5-cvc5-xyz ^ne	117 (base -30)	8076.00	8091.06	117	117	81	102	81
OpenSMT-SMTS-seq-base ⁿ	179	17082.62	17106.60	179	179	19	102	19
z3-BooledASS-base ⁿ	173	9579.98	9602.17	173	173	25	102	25
cvc5-cvc5-xyz-base ⁿ	147	12860.18	12879.69	147	147	51	102	51

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
z3-BooledASS ^ne	230 (base +0)	278.62	306.65	230	86	144	70
OpenSMT	202	749.20	774.25	202	79	123	98
OpenSMT-SMTS-seq ^ne	197 (base -5)	735.07	742.44	197	77	120	103
SMTInterpol	197	2397.03	1030.91	197	83	114	103
Yices2	194	102.39	126.34	194	48	146	106
cvc5	154	433.78	452.80	154	49	105	146
cvc5-cvc5-xyz	129 (base -25)	284.60	300.36	129	48	81	171
z3-BooledASS-base ⁿ	230	279.59	308.00	230	86	144	70
OpenSMT-SMTS-seq-base ⁿ	202	759.05	784.16	202	79	123	98
cvc5-cvc5-xyz-base ⁿ	154	446.48	465.54	154	49	105	146

SMT-COMP 2026