QF_FPArith (Model Validation Track)

Competition results for the QF_FPArith division in the Model Validation Track.

Page generated on 2022-08-10 11:19:11 +0000

Benchmarks: 17301
Time Limit: 1200 seconds
Memory Limit: 60 GB

Logics:

• QF_BVFP : 7028 benchmarks
• QF_BVFPLRA : 116 benchmarks
• QF_FP : 10106 benchmarks
• QF_FPLRA : 51 benchmarks

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Bitwuzla	0	17294	12477.011	12568.011		4	0
cvc5	0	17271	23574.227	23566.761		12	0
z3-4.8.17n	0	17254	56643.884	63016.082		25	2
MathSATn	0	15796	32921.333	32856.932		21	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Bitwuzla	0	17294	12478.851	12567.751		4	0
cvc5	0	17271	23576.957	23566.201		12	0
z3-4.8.17n	0	17254	57246.664	63014.862		25	2
MathSATn	0	15796	32924.493	32855.932		21	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.