QF_FPArith (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +0000

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

Logics:

• QF_ABVFP : 600 benchmarks
• QF_ABVFPLRA : 25 benchmarks
• QF_AUFBVFP : 1 benchmarks
• QF_BVFP : 465 benchmarks
• QF_BVFPLRA : 69 benchmarks
• QF_FP : 285 benchmarks
• QF_FPLRA : 55 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Bitwuzla	Bitwuzla	Bitwuzla	Bitwuzla	Bitwuzla

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	1439	82604.868	82577.783	1439	549	890	61	0	45	0
cvc5	0	1429	132292.259	132136.806	1429	549	880	71	0	71	0
2021-cvc5n	0	1423	133834.826	133708.602	1423	542	881	77	0	77	0
MathSATn	0	1386	159982.817	159934.201	1386	534	852	114	0	103	0
z3-4.8.17n	0	1316	294174.216	304576.623	1316	504	812	184	0	156	4
COLIBRI	0	1267	144280.522	144248.226	1267	516	751	232	1	112	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	1439	82610.638	82576.183	1439	549	890	61	0	45	0
cvc5	0	1429	132305.219	132133.386	1429	549	880	71	0	71	0
2021-cvc5n	0	1423	133847.276	133704.732	1423	542	881	77	0	77	0
MathSATn	0	1386	160001.767	159929.901	1386	534	852	114	0	103	0
z3-4.8.17n	0	1316	294675.736	304569.523	1316	504	812	184	0	156	4
COLIBRI	0	1267	144280.522	144248.226	1267	516	751	232	1	112	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	549	13236.788	13231.952	549	549	0	14	937	45	0
cvc5	0	549	29685.159	29659.447	549	549	0	14	937	71	0
2021-cvc5n	0	542	35449.638	35407.377	542	542	0	21	937	77	0
MathSATn	0	534	39717.309	39716.76	534	534	0	29	937	103	0
COLIBRI	0	516	35992.866	35976.572	516	516	0	46	938	112	0
z3-4.8.17n	0	504	88235.967	95171.904	504	504	0	59	937	156	4

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	890	57373.85	57344.231	890	0	890	37	573	45	0
2021-cvc5n	0	881	86397.638	86297.354	881	0	881	46	573	77	0
cvc5	0	880	90620.06	90473.939	880	0	880	47	573	71	0
MathSATn	0	852	108284.458	108213.141	852	0	852	75	573	103	0
z3-4.8.17n	0	812	194439.769	197397.619	812	0	812	115	573	156	4
COLIBRI	0	751	96287.655	96271.654	751	0	751	176	573	112	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	1328	5623.635	5584.682	1328	506	822	172	0	156	0
COLIBRI	0	1232	6305.487	6272.508	1232	505	727	267	1	148	0
MathSATn	0	1229	9755.24	9717.128	1229	463	766	271	0	260	0
2021-cvc5n	0	1218	11580.342	11431.629	1218	484	734	282	0	282	0
cvc5	0	1192	11839.632	11701.886	1192	463	729	308	0	308	0
z3-4.8.17n	0	898	18246.092	18236.577	898	376	522	602	0	598	4

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.