QF_FPArith (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

QF_ABVFP : 525 benchmarks
QF_ABVFPLRA : 25 benchmarks
QF_AUFBVFP : 1 benchmarks
QF_BVFP : 505 benchmarks
QF_BVFPLRA : 75 benchmarks
QF_FP : 275 benchmarks
QF_FPLRA : 55 benchmarks
QF_UFFPDTNIRA : 15 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	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	0	1440	20121.42	20302.90	1440	576	864	21	15	21
cvc5	0	1407	46400.80	46580.08	1407	572	835	69	0	69
cvc5-cvc5-xyz ^ne	0	1407 (base +1)	47286.48	47464.70	1407	572	835	69	0	69
colibri2	0	1095	17325.95	17462.35	1095	445	650	381	0	114
bitwuzla-dandelion ⁿ	0	815 (base -623)	17809.98	17913.82	815	418	397	646	15	20
z3-BooledASS ^ne	0	53 (base -1226)	29.50	36.04	53	1	52	1423	0	128
COLIBRI	12	1262	7096.64	7254.13	1274	538	736	202	0	75
bitwuzla-dandelion-base ⁿ	0	1438	21407.03	21587.82	1438	576	862	23	15	23
cvc5-cvc5-xyz-base ⁿ	0	1406	46145.77	46325.18	1406	571	835	70	0	70
z3-BooledASS-base ⁿ	0	1279	97415.13	97582.72	1279	508	771	197	0	153

(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	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	0	1440	20121.42	20302.90	1440	576	864	21	15	21
cvc5	0	1407	46400.80	46580.08	1407	572	835	69	0	69
cvc5-cvc5-xyz ^ne	0	1407 (base +1)	47286.48	47464.70	1407	572	835	69	0	69
colibri2	0	1095	17325.95	17462.35	1095	445	650	381	0	114
bitwuzla-dandelion ⁿ	0	815 (base -623)	17809.98	17913.82	815	418	397	646	15	20
z3-BooledASS ^ne	0	53 (base -1226)	29.50	36.04	53	1	52	1423	0	128
COLIBRI	12	1262	7096.64	7254.13	1274	538	736	202	0	75
bitwuzla-dandelion-base ⁿ	0	1438	21407.03	21587.82	1438	576	862	23	15	23
cvc5-cvc5-xyz-base ⁿ	0	1406	46145.77	46325.18	1406	571	835	70	0	70
z3-BooledASS-base ⁿ	0	1279	97415.13	97582.72	1279	508	771	197	0	153

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	0	576	7566.26	7639.15	576	576	0	6	894	6
cvc5-cvc5-xyz ^ne	0	572 (base +1)	11640.93	11712.69	572	572	0	13	891	13
cvc5	0	572	11649.75	11721.95	572	572	0	13	891	13
colibri2	0	445	7603.47	7658.92	445	445	0	140	891	17
bitwuzla-dandelion ⁿ	0	418 (base -158)	9502.98	9556.28	418	418	0	164	894	3
z3-BooledASS ^ne	0	1 (base -507)	2.54	2.66	1	1	0	584	891	52
COLIBRI	12	538	2890.17	2958.28	550	538	12	35	891	10
bitwuzla-dandelion-base ⁿ	0	576	7980.45	8052.94	576	576	0	6	894	6
cvc5-cvc5-xyz-base ⁿ	0	571	10449.20	10521.44	571	571	0	14	891	14
z3-BooledASS-base ⁿ	0	508	29872.28	29938.07	508	508	0	77	891	48

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	864	12555.17	12663.75	864	864	6	606	6
cvc5	835	34751.05	34858.13	835	835	47	594	47
cvc5-cvc5-xyz ^ne	835 (base +0)	35645.55	35752.01	835	835	47	594	47
COLIBRI	721	4011.34	4100.33	721	721	161	594	59
colibri2	650	9722.48	9803.43	650	650	232	594	95
bitwuzla-dandelion ⁿ	397 (base -465)	8306.99	8357.54	397	397	473	606	8
z3-BooledASS ^ne	52 (base -719)	26.96	33.38	52	52	830	594	71
bitwuzla-dandelion-base ⁿ	862	13426.59	13534.88	862	862	8	606	8
cvc5-cvc5-xyz-base ⁿ	835	35696.56	35803.74	835	835	47	594	47
z3-BooledASS-base ⁿ	771	67542.85	67644.65	771	771	111	594	100

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Bitwuzla	0	1351	1664.44	1831.48	1351	536	815	0	125
cvc5-cvc5-xyz ^ne	0	1201 (base +0)	3488.20	3636.38	1201	497	704	0	275
cvc5	0	1200	3453.13	3602.03	1200	496	704	0	276
colibri2	0	1037	1349.12	1476.88	1037	424	613	225	214
bitwuzla-dandelion ⁿ	0	738 (base -615)	1063.94	1156.20	738	375	363	626	112
z3-BooledASS ^ne	0	53 (base -897)	29.50	36.04	53	1	52	1131	292
COLIBRI	12	1223	1917.29	2069.38	1235	522	713	127	114
bitwuzla-dandelion-base ⁿ	0	1353	1643.96	1811.98	1353	533	820	0	123
cvc5-cvc5-xyz-base ⁿ	0	1201	3500.44	3650.00	1201	497	704	0	275
z3-BooledASS-base ⁿ	0	950	3758.88	3876.71	950	399	551	0	526

SMT-COMP 2026