FPArith (Single Query Track)

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

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

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

Logics:

• BVFP : 205 benchmarks
• BVFPLRA : 185 benchmarks
• FP : 1340 benchmarks
• FPLRA : 27 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	1426	387808.515	404618.477	1426	333	1093	331	0	295	0
2020-CVC4n	0	1164	470897.88	470977.592	1164	302	862	593	0	358	0
z3n	0	1105	350499.091	350541.589	1105	90	1015	235	417	232	0
UltimateEliminator+MathSAT	0	241	40483.653	37937.147	241	63	178	1516	0	24	0
2019-Z3n	0	0	376628.682	376620.951	0	0	0	1545	212	220	36

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	1426	403573.732	404604.597	1426	333	1093	331	0	295	0
2020-CVC4n	0	1164	470968.29	470961.012	1164	302	862	593	0	358	0
z3n	0	1105	350581.881	350531.859	1105	90	1015	235	417	232	0
UltimateEliminator+MathSAT	0	241	40483.653	37937.147	241	63	178	1516	0	24	0
2019-Z3n	0	0	376673.502	376611.581	0	0	0	1545	212	220	36

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	333	49148.194	49161.471	333	333	0	22	1402	295	0
2020-CVC4n	0	302	73108.091	73112.9	302	302	0	53	1402	358	0
z3n	0	90	67278.528	67304.999	90	90	0	28	1639	232	0
UltimateEliminator+MathSAT	0	63	2257.192	2093.614	63	63	0	292	1402	24	0
2019-Z3n	0	0	74146.732	74147.116	0	0	0	241	1516	220	36

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	1093	59212.999	60230.595	1093	0	1093	28	636	295	0
z3n	0	1015	151282.089	151205.592	1015	0	1015	94	648	232	0
2020-CVC4n	0	862	178190.488	178178.408	862	0	862	259	636	358	0
UltimateEliminator+MathSAT	0	178	6366.496	4376.265	178	0	178	943	636	24	0
2019-Z3n	0	0	154944.192	154880.952	0	0	0	1116	641	220	36

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	1266	12875.104	12818.857	1266	267	999	491	0	455	0
2020-CVC4n	0	1022	13911.073	13897.207	1022	227	795	735	0	500	0
z3n	0	877	12964.872	12936.664	877	5	872	463	417	460	0
UltimateEliminator+MathSAT	0	235	10148.483	7633.08	235	57	178	1522	0	36	0
2019-Z3n	0	0	14711.616	14682.561	0	0	0	1545	212	480	36

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.