QF_FPArith (Single Query Track)

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

Page generated on 2023-07-06 16:04:54 +0000

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

Logics:

• QF_ABVFP : 593 benchmarks
• QF_ABVFPLRA : 25 benchmarks
• QF_AUFBVFP : 1 benchmarks
• QF_BVFP : 414 benchmarks
• QF_BVFPLRA : 78 benchmarks
• QF_FP : 273 benchmarks
• QF_FPLRA : 58 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	1386	27893.071	27844.487	1386	507	879	56	0	56	0
Bitwuzla Fixedn	0	1386	27980.926	27918.632	1386	507	879	56	0	56	0
2022-Bitwuzlan	0	1374	26288.753	26293.004	1374	497	877	68	0	52	0
cvc5	0	1258	52579.513	52543.216	1258	474	784	184	0	81	0
COLIBRI	0	1206	4372.757	4345.033	1206	463	743	236	0	110	0
Z3-Owl Fixedn	0	570	55841.523	55756.141	570	253	317	117	755	117	0
Z3-Owl	357	330	269.291	269.287	330	304	26	357	755	0	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	1386	27893.071	27844.487	1386	507	879	56	0	56	0
Bitwuzla Fixedn	0	1386	27980.926	27918.632	1386	507	879	56	0	56	0
2022-Bitwuzlan	0	1374	26288.753	26293.004	1374	497	877	68	0	52	0
cvc5	0	1258	52579.513	52543.216	1258	474	784	184	0	81	0
COLIBRI	0	1206	4372.757	4345.033	1206	463	743	236	0	110	0
Z3-Owl Fixedn	0	570	55841.523	55756.141	570	253	317	117	755	117	0
Z3-Owl	357	330	269.291	269.287	330	304	26	357	755	0	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	507	7848.161	7840.731	507	507	0	19	916	56	0
Bitwuzla Fixedn	0	507	7870.581	7863.488	507	507	0	19	916	56	0
2022-Bitwuzlan	0	497	8814.264	8816.302	497	497	0	29	916	52	0
cvc5	0	474	10760.374	10730.279	474	474	0	52	916	81	0
COLIBRI	0	463	2288.653	2283.283	463	463	0	63	916	110	0
Z3-Owl Fixedn	0	253	23721.218	23683.438	253	253	0	51	1138	117	0
Z3-Owl	357	304	217.641	217.619	304	304	0	0	1138	0	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	879	20044.91	20003.756	879	0	879	37	526	56	0
Bitwuzla Fixedn	0	879	20110.345	20055.145	879	0	879	37	526	56	0
2022-Bitwuzlan	0	877	17474.49	17476.702	877	0	877	39	526	52	0
cvc5	0	784	41819.138	41812.938	784	0	784	132	526	81	0
COLIBRI	0	743	2084.104	2061.75	743	0	743	173	526	110	0
Z3-Owl Fixedn	0	317	32120.305	32072.703	317	0	317	66	1059	117	0
Z3-Owl	0	26	51.65	51.668	26	0	26	357	1059	0	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 Fixedn	0	1285	2011.323	1997.134	1285	467	818	157	0	157	0
Bitwuzla	0	1285	2050.61	1998.073	1285	467	818	157	0	157	0
2022-Bitwuzlan	0	1267	1857.481	1857.169	1267	456	811	175	0	159	0
COLIBRI	0	1183	2382.68	2354.708	1183	451	732	259	0	133	0
cvc5	0	985	4210.14	4165.121	985	387	598	457	0	354	0
Z3-Owl Fixedn	0	301	2868.139	2848.425	301	132	169	386	755	386	0
Z3-Owl	357	330	269.291	269.287	330	304	26	357	755	0	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.