FPArith (Single Query Track)

Competition results for the FPArith division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

BVFP : 208 benchmarks
BVFPLRA : 266 benchmarks
FP : 664 benchmarks
FPLRA : 40 benchmarks

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	Abstained	Timeout
Bitwuzla	1142	11754.57	11898.64	1142	537	605	36	0	36
cvc5	1101	24250.81	24389.01	1101	500	601	77	0	74
cvc5-cvc5-xyz ^ne	1100 (base +0)	23072.30	23210.22	1100	499	601	78	0	75
z3-BooledASS ^ne	522 (base -502)	19394.89	19461.03	522	2	520	656	0	91
Bitwuzla-fixed ⁿ	469	115.26	172.90	469	432	37	5	704	5
bitwuzla-dandelion ⁿ	439 (base -484)	13622.73	13678.97	439	69	370	739	0	37
colibri2	269	2222.70	2255.97	269	116	153	909	0	28
UltimateEliminator+MathSAT	166	19692.97	19269.17	166	84	82	1012	0	53
cvc5-cvc5-xyz-base ⁿ	1100	23154.27	23292.66	1100	499	601	78	0	75
z3-BooledASS-base ⁿ	1024	39579.03	39709.03	1024	464	560	154	0	138
bitwuzla-dandelion-base ⁿ	923	16453.13	16570.09	923	516	407	255	0	67

(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	Abstained	Timeout
Bitwuzla	1142	11754.57	11898.64	1142	537	605	36	0	36
cvc5	1101	24250.81	24389.01	1101	500	601	77	0	74
cvc5-cvc5-xyz ^ne	1100 (base +0)	23072.30	23210.22	1100	499	601	78	0	75
z3-BooledASS ^ne	522 (base -502)	19394.89	19461.03	522	2	520	656	0	91
Bitwuzla-fixed ⁿ	469	115.26	172.90	469	432	37	5	704	5
bitwuzla-dandelion ⁿ	439 (base -484)	13622.73	13678.97	439	69	370	739	0	37
colibri2	269	2222.70	2255.97	269	116	153	909	0	28
UltimateEliminator+MathSAT	166	19692.97	19269.17	166	84	82	1012	0	53
cvc5-cvc5-xyz-base ⁿ	1100	23154.27	23292.66	1100	499	601	78	0	75
z3-BooledASS-base ⁿ	1024	39579.03	39709.03	1024	464	560	154	0	138
bitwuzla-dandelion-base ⁿ	923	16453.13	16570.09	923	516	407	255	0	67

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Bitwuzla	537	5529.96	5597.67	537	537	2	639	2
cvc5	500	16874.97	16938.16	500	500	39	639	37
cvc5-cvc5-xyz ^ne	499 (base +0)	15647.78	15710.76	499	499	40	639	38
Bitwuzla-fixed ⁿ	432	88.07	141.15	432	432	2	744	2
colibri2	116	2194.47	2208.89	116	116	423	639	26
UltimateEliminator+MathSAT	84	18720.31	18488.24	84	84	455	639	43
bitwuzla-dandelion ⁿ	69 (base -447)	6150.15	6159.48	69	69	470	639	0
z3-BooledASS ^ne	2 (base -462)	65.04	65.29	2	2	537	639	21
bitwuzla-dandelion-base ⁿ	516	6819.69	6884.73	516	516	23	639	23
cvc5-cvc5-xyz-base ⁿ	499	15707.96	15771.15	499	499	40	639	38
z3-BooledASS-base ⁿ	464	14855.18	14913.69	464	464	75	639	67

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	605	6224.62	6300.97	605	605	9	564	9
cvc5	601	7375.84	7450.85	601	601	13	564	12
cvc5-cvc5-xyz ^ne	601 (base +0)	7424.53	7499.46	601	601	13	564	12
z3-BooledASS ^ne	520 (base -40)	19329.85	19395.74	520	520	94	564	51
bitwuzla-dandelion ⁿ	370 (base -37)	7472.59	7519.49	370	370	244	564	17
colibri2	153	28.23	47.08	153	153	461	564	2
UltimateEliminator+MathSAT	82	972.67	780.93	82	82	532	564	3
Bitwuzla-fixed ⁿ	37	27.18	31.76	37	37	2	1139	2
cvc5-cvc5-xyz-base ⁿ	601	7446.31	7521.51	601	601	13	564	12
z3-BooledASS-base ⁿ	560	24723.85	24795.34	560	560	54	564	53
bitwuzla-dandelion-base ⁿ	407	9633.44	9685.36	407	407	207	564	19

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla	1067	844.00	976.72	1067	488	579	0	111
cvc5	1038	1070.56	1198.70	1038	460	578	2	138
cvc5-cvc5-xyz ^ne	1037 (base +0)	1085.02	1212.93	1037	460	577	2	139
Bitwuzla-fixed ⁿ	469	115.26	172.90	469	432	37	0	709
z3-BooledASS ^ne	454 (base -414)	745.33	801.18	454	1	453	515	209
bitwuzla-dandelion ⁿ	363 (base -481)	572.48	617.65	363	19	344	702	113
colibri2	251	68.64	99.51	251	98	153	842	85
UltimateEliminator+MathSAT	138	735.77	415.60	138	57	81	953	87
cvc5-cvc5-xyz-base ⁿ	1037	1095.46	1223.66	1037	460	577	2	139
z3-BooledASS-base ⁿ	868	1531.55	1638.26	868	390	478	9	301
bitwuzla-dandelion-base ⁿ	844	596.46	701.58	844	463	381	188	146

SMT-COMP 2026