QF_FPArith (Single Query Track)

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

Page generated on 2021-07-18 17:29:06 +0000

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

Logics:

• QF_ABVFP : 619 benchmarks
• QF_ABVFPLRA : 25 benchmarks
• QF_AUFBVFP : 1 benchmarks
• QF_BVFP : 484 benchmarks
• QF_BVFPLRA : 72 benchmarks
• QF_FP : 300 benchmarks
• QF_FPLRA : 55 benchmarks
• QF_UFFPDTLIRA : 154 benchmarks

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	1636	128495.002	128362.236	1636	651	985	74	0	74	0
Bitwuzla	0	1495	81171.945	81167.437	1495	626	869	61	154	45	0
2020-CVC4n	0	1456	148876.731	148799.658	1456	615	841	99	155	99	0
MathSAT5n	0	1453	138338.363	138230.142	1453	618	835	103	154	92	0
2020-MathSAT5n	0	1452	139375.054	139212.413	1452	617	835	103	155	92	0
2020-Bitwuzlan	0	1375	59251.817	59190.449	1375	530	845	28	307	28	0
2020-Bitwuzla-fixedn	0	1373	59166.876	59123.416	1373	530	843	30	307	30	0
COLIBRI - fixedn	0	1354	89285.401	89278.969	1354	598	756	202	154	67	0
z3n	0	730	156929.918	162278.244	730	417	313	109	871	90	7
cvc5 - fixedn	0	154	123.536	123.556	154	24	130	0	1556	0	0
2020-COLIBRIn	3	1326	114065.119	114007.433	1326	583	743	229	155	91	0
COLIBRI	8	1346	87665.248	87619.359	1346	587	759	210	154	67	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	1636	128505.532	128359.586	1636	651	985	74	0	74	0
Bitwuzla	0	1495	81176.575	81166.117	1495	626	869	61	154	45	0
2020-CVC4n	0	1456	148897.031	148795.208	1456	615	841	99	155	99	0
MathSAT5n	0	1453	138422.013	138225.992	1453	618	835	103	154	92	0
2020-MathSAT5n	0	1452	139392.564	139208.453	1452	617	835	103	155	92	0
2020-Bitwuzlan	0	1375	59255.857	59189.389	1375	530	845	28	307	28	0
2020-Bitwuzla-fixedn	0	1373	59169.946	59122.656	1373	530	843	30	307	30	0
COLIBRI - fixedn	0	1354	89291.491	89276.459	1354	598	756	202	154	67	0
z3n	0	730	157028.598	162273.924	730	417	313	109	871	90	7
cvc5 - fixedn	0	154	123.536	123.556	154	24	130	0	1556	0	0
2020-COLIBRIn	3	1326	114074.219	114004.723	1326	583	743	229	155	91	0
COLIBRI	8	1346	87671.158	87617.629	1346	587	759	210	154	67	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	651	28877.058	28864.287	651	651	0	16	1043	74	0
Bitwuzla	0	626	14413.933	14411.94	626	626	0	17	1067	45	0
MathSAT5n	0	618	32042.97	31956.768	618	618	0	25	1067	92	0
2020-MathSAT5n	0	617	32433.308	32416.725	617	617	0	25	1068	92	0
2020-CVC4n	0	615	44655.119	44654.364	615	615	0	27	1068	99	0
COLIBRI - fixedn	0	598	28015.917	28004.766	598	598	0	45	1067	67	0
COLIBRI	0	587	31468.942	31429.659	587	587	0	56	1067	67	0
2020-Bitwuzla-fixedn	0	530	10486.319	10436.415	530	530	0	2	1178	30	0
2020-Bitwuzlan	0	530	10472.666	10472.256	530	530	0	2	1178	28	0
z3n	0	417	66126.767	71427.343	417	417	0	45	1248	90	7
cvc5 - fixedn	0	24	67.135	67.176	24	24	0	0	1686	0	0
2020-COLIBRIn	3	583	41257.23	41206.417	583	583	0	59	1068	91	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	985	88828.474	88695.299	985	0	985	49	676	74	0
Bitwuzla	0	869	55962.642	55954.177	869	0	869	35	806	45	0
2020-Bitwuzlan	0	845	37983.191	37917.133	845	0	845	17	848	28	0
2020-Bitwuzla-fixedn	0	843	37883.626	37886.241	843	0	843	19	848	30	0
2020-CVC4n	0	841	93441.912	93340.844	841	0	841	63	806	99	0
MathSAT5n	0	835	95579.043	95469.223	835	0	835	69	806	92	0
2020-MathSAT5n	0	835	96159.256	95991.728	835	0	835	69	806	92	0
COLIBRI - fixedn	0	756	50475.574	50471.694	756	0	756	148	806	67	0
2020-COLIBRIn	0	743	62304.029	62285.209	743	0	743	161	806	91	0
z3n	0	313	82501.831	82446.581	313	0	313	57	1340	90	7
cvc5 - fixedn	0	130	56.402	56.38	130	0	130	0	1580	0	0
COLIBRI	8	759	45402.216	45387.97	759	0	759	145	806	67	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	1425	11144.475	11088.701	1425	587	838	285	0	285	0
Bitwuzla	0	1397	5120.567	5106.358	1397	588	809	159	154	143	0
2020-CVC4n	0	1332	8771.178	8742.62	1332	554	778	223	155	223	0
COLIBRI - fixedn	0	1328	4747.715	4731.401	1328	586	742	228	154	97	0
MathSAT5n	0	1318	8590.156	8552.234	1318	556	762	238	154	227	0
2020-MathSAT5n	0	1313	8726.75	8622.464	1313	552	761	242	155	231	0
2020-Bitwuzla-fixedn	0	1288	4266.279	4263.675	1288	495	793	115	307	115	0
2020-Bitwuzlan	0	1287	4274.653	4263.76	1287	494	793	116	307	116	0
z3n	0	564	8251.01	8246.887	564	320	244	275	871	268	7
cvc5 - fixedn	0	153	87.967	87.984	153	23	130	1	1556	1	0
2020-COLIBRIn	3	1296	5140.831	5097.601	1296	574	722	259	155	122	0
COLIBRI	8	1331	4464.313	4443.364	1331	577	754	225	154	86	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.