FP (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 664
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	Bitwuzla	Bitwuzla	Bitwuzla

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Bitwuzla	637	11626.26	11707.78	637	69	568	27	27
cvc5	618	20500.86	20579.06	618	56	562	46	45
cvc5-cvc5-xyz ^ne	617 (base +0)	19315.79	19393.82	617	55	562	47	46
z3-BooledASS ^ne	522 (base -47)	19394.89	19461.03	522	2	520	142	91
bitwuzla-dandelion ⁿ	439 (base +0)	13622.73	13678.97	439	69	370	225	37
colibri2	162	2200.92	2221.05	162	25	137	502	13
UltimateEliminator+MathSAT	102	19165.95	18906.34	102	25	77	562	52
cvc5-cvc5-xyz-base ⁿ	617	19401.94	19480.20	617	55	562	47	46
z3-BooledASS-base ⁿ	569	32725.99	32799.47	569	47	522	95	90
bitwuzla-dandelion-base ⁿ	439	16186.93	16243.58	439	69	370	225	37

(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	637	11626.26	11707.78	637	69	568	27	27
cvc5	618	20500.86	20579.06	618	56	562	46	45
cvc5-cvc5-xyz ^ne	617 (base +0)	19315.79	19393.82	617	55	562	47	46
z3-BooledASS ^ne	522 (base -47)	19394.89	19461.03	522	2	520	142	91
bitwuzla-dandelion ⁿ	439 (base +0)	13622.73	13678.97	439	69	370	225	37
colibri2	162	2200.92	2221.05	162	25	137	502	13
UltimateEliminator+MathSAT	102	19165.95	18906.34	102	25	77	562	52
cvc5-cvc5-xyz-base ⁿ	617	19401.94	19480.20	617	55	562	47	46
z3-BooledASS-base ⁿ	569	32725.99	32799.47	569	47	522	95	90
bitwuzla-dandelion-base ⁿ	439	16186.93	16243.58	439	69	370	225	37

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	69	5428.98	5438.72	69	69	0	595	0
bitwuzla-dandelion ⁿ	69 (base +0)	6150.15	6159.48	69	69	0	595	0
cvc5	56	14414.12	14422.29	56	56	13	595	13
cvc5-cvc5-xyz ^ne	55 (base +0)	13181.29	13189.36	55	55	14	595	14
colibri2	25	2175.61	2178.85	25	25	44	595	13
UltimateEliminator+MathSAT	25	18259.02	18164.53	25	25	44	595	43
z3-BooledASS ^ne	2 (base -45)	65.04	65.29	2	2	67	595	21
bitwuzla-dandelion-base ⁿ	69	6698.58	6707.95	69	69	0	595	0
cvc5-cvc5-xyz-base ⁿ	55	13245.09	13253.15	55	55	14	595	14
z3-BooledASS-base ⁿ	47	9775.68	9782.53	47	47	22	595	22

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	568	6197.29	6269.06	568	568	7	89	7
cvc5	562	6086.74	6156.77	562	562	13	89	12
cvc5-cvc5-xyz ^ne	562 (base +0)	6134.50	6204.47	562	562	13	89	12
z3-BooledASS ^ne	520 (base -2)	19329.85	19395.74	520	520	55	89	51
bitwuzla-dandelion ⁿ	370 (base +0)	7472.59	7519.49	370	370	205	89	17
colibri2	137	25.30	42.20	137	137	438	89	0
UltimateEliminator+MathSAT	77	906.93	741.81	77	77	498	89	3
cvc5-cvc5-xyz-base ⁿ	562	6156.86	6227.05	562	562	13	89	12
z3-BooledASS-base ⁿ	522	22950.31	23016.94	522	522	53	89	52
bitwuzla-dandelion-base ⁿ	370	9488.35	9535.64	370	370	205	89	17

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla	562	715.70	785.86	562	20	542	0	102
cvc5	562	838.49	907.87	562	20	542	0	102
cvc5-cvc5-xyz ^ne	561 (base +0)	842.02	911.33	561	20	541	0	103
z3-BooledASS	454 (base +0)	745.33	801.18	454	1	453	1	209
bitwuzla-dandelion ⁿ	363 (base +1)	572.48	617.65	363	19	344	188	113
colibri2	144	46.85	64.59	144	7	137	452	68
UltimateEliminator+MathSAT	77	314.33	150.21	77	1	76	506	81
cvc5-cvc5-xyz-base ⁿ	561	850.44	919.82	561	20	541	0	103
z3-BooledASS-base ⁿ	454	904.34	960.23	454	1	453	1	209
bitwuzla-dandelion-base ⁿ	362	477.68	522.77	362	17	345	188	114

SMT-COMP 2026