QF_FPArith (Unsat Core Track)

Competition results for the QF_FPArith division in the Unsat Core Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_ABVFP : 793 benchmarks
QF_ABVFPLRA : 2 benchmarks
QF_BVFP : 717 benchmarks
QF_BVFPLRA : 52 benchmarks
QF_FP : 2406 benchmarks
QF_UFFP : 2 benchmarks
QF_UFFPDTNIRA : 4 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Bitwuzla	Bitwuzla	-	Bitwuzla	Bitwuzla

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	15658	4701.06	5196.00	3969	3969	3	4	3
cvc5	15019	11558.98	12052.59	3970	3970	6	0	6
z3-BooledASS ^ne	6266 (base -7441)	24625.72	25011.34	3109	3109	867	0	14
z3-BooledASS-base ⁿ	13707	47850.08	48340.64	3936	3936	40	0	40

(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 UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	15658	4701.06	5196.00	3969	3969	3	4	3
cvc5	15019	11558.98	12052.59	3970	3970	6	0	6
z3-BooledASS ^ne	6266 (base -7441)	24625.72	25011.34	3109	3109	867	0	14
z3-BooledASS-base ⁿ	13707	47850.08	48340.64	3936	3936	40	0	40

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Bitwuzla	15658	4701.06	5196.00	3969	3969	3	4	3
cvc5	15019	11558.98	12052.59	3970	3970	6	0	6
z3-BooledASS ^ne	6266 (base -7441)	24625.72	25011.34	3109	3109	867	0	14
z3-BooledASS-base ⁿ	13707	47850.08	48340.64	3936	3936	40	0	40

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained
Bitwuzla	14525	1441.59	1934.82	3959	3959	0	17
cvc5	12718	1781.87	2269.48	3928	3928	0	48
z3-BooledASS ^ne	6200 (base -5925)	1693.07	2051.32	2909	2909	853	214
z3-BooledASS-base ⁿ	12125	2967.64	3415.82	3632	3632	0	344

SMT-COMP 2026