QF_FP (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
bitwuzla-dandelion ⁿ	256 (base +0)	15795.06	15829.01	256	140	116	19	19
Bitwuzla	255	14222.61	14257.00	255	137	118	20	20
COLIBRI	239	3199.57	3229.39	239	135	104	36	36
cvc5	232	21184.05	21215.12	232	140	92	43	43
cvc5-cvc5-xyz ^ne	232 (base +1)	21226.50	21257.51	232	140	92	43	43
colibri2	200	6648.83	6674.07	200	119	81	75	9
z3-BooledASS ^ne	3 (base -157)	14.20	14.58	3	0	3	272	94
bitwuzla-dandelion-base ⁿ	256	14968.12	15001.76	256	139	117	19	19
cvc5-cvc5-xyz-base ⁿ	231	20052.56	20083.40	231	139	92	44	44
z3-BooledASS-base ⁿ	160	22265.51	22287.42	160	93	67	115	84

(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
bitwuzla-dandelion ⁿ	256 (base +0)	15795.06	15829.01	256	140	116	19	19
Bitwuzla	255	14222.61	14257.00	255	137	118	20	20
COLIBRI	239	3199.57	3229.39	239	135	104	36	36
cvc5	232	21184.05	21215.12	232	140	92	43	43
cvc5-cvc5-xyz ^ne	232 (base +1)	21226.50	21257.51	232	140	92	43	43
colibri2	200	6648.83	6674.07	200	119	81	75	9
z3-BooledASS ^ne	3 (base -157)	14.20	14.58	3	0	3	272	94
bitwuzla-dandelion-base ⁿ	256	14968.12	15001.76	256	139	117	19	19
cvc5-cvc5-xyz-base ⁿ	231	20052.56	20083.40	231	139	92	44	44
z3-BooledASS-base ⁿ	160	22265.51	22287.42	160	93	67	115	84

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	140 (base +1)	7255.20	7273.35	140	140	3	132	3
cvc5	140	7263.63	7281.77	140	140	3	132	3
bitwuzla-dandelion ⁿ	140 (base +1)	8084.62	8103.22	140	140	3	132	3
Bitwuzla	137	5310.93	5329.17	137	137	6	132	6
COLIBRI	135	2179.66	2196.53	135	135	8	132	8
colibri2	119	5840.52	5855.70	119	119	24	132	6
z3-BooledASS ^ne	0 (base -93)	0.00	0.00	0	0	143	132	35
cvc5-cvc5-xyz-base ⁿ	139	6054.34	6072.23	139	139	4	132	4
bitwuzla-dandelion-base ⁿ	139	6747.62	6765.72	139	139	4	132	4
z3-BooledASS-base ⁿ	93	12202.24	12214.96	93	93	50	132	31

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	118	8911.68	8927.83	118	118	6	151	6
bitwuzla-dandelion ⁿ	116 (base -1)	7710.44	7725.80	116	116	8	151	8
COLIBRI	102	825.13	837.80	102	102	22	151	22
cvc5	92	13920.42	13933.35	92	92	32	151	32
cvc5-cvc5-xyz ^ne	92 (base +0)	13971.30	13984.16	92	92	32	151	32
colibri2	81	808.31	818.37	81	81	43	151	1
z3-BooledASS ^ne	3 (base -64)	14.20	14.58	3	3	121	151	55
bitwuzla-dandelion-base ⁿ	117	8220.51	8236.03	117	117	7	151	7
cvc5-cvc5-xyz-base ⁿ	92	13998.23	14011.17	92	92	32	151	32
z3-BooledASS-base ⁿ	67	10063.27	10072.46	67	67	57	151	49

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
COLIBRI	220	480.29	507.42	220	122	98	0	55
Bitwuzla	193	681.33	705.36	193	105	88	0	82
bitwuzla-dandelion ⁿ	190 (base -6)	633.35	657.19	190	104	86	0	85
colibri2	174	231.72	253.19	174	104	70	62	39
cvc5-cvc5-xyz ^ne	164 (base +0)	770.92	791.23	164	103	61	0	111
cvc5	164	771.61	791.95	164	103	61	0	111
z3-BooledASS ^ne	3 (base -70)	14.20	14.58	3	0	3	68	204
bitwuzla-dandelion-base ⁿ	196	742.74	767.17	196	106	90	0	79
cvc5-cvc5-xyz-base ⁿ	164	773.29	793.73	164	103	61	0	111
z3-BooledASS-base ⁿ	73	528.07	537.19	73	52	21	0	202

SMT-COMP 2026