UFLRA (Single Query Track)

Competition results for the UFLRA logic in the Single Query Track.

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

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
veriT	veriT	—	veriT	veriT

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	6	2127.919	2128.311	6	4	2	1	1	0
2020-CVC4n	0	3	5369.456	5371.287	3	1	2	4	4	0
veriT	0	2	4799.965	4800.444	2	0	2	5	4	0
smtinterpol	0	2	4801.944	4801.261	2	0	2	5	4	0
cvc5	0	2	5810.556	5819.435	2	0	2	5	4	0
Vampire	0	2	6000.293	6000.567	2	0	2	5	5	0
UltimateEliminator+MathSAT	0	0	32.986	21.228	0	0	0	7	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	6	2128.109	2128.291	6	4	2	1	1	0
2020-CVC4n	0	3	5370.736	5371.127	3	1	2	4	4	0
veriT	0	2	4800.345	4800.344	2	0	2	5	4	0
smtinterpol	0	2	4801.944	4801.261	2	0	2	5	4	0
cvc5	0	2	5816.246	5819.155	2	0	2	5	4	0
Vampire	0	2	6000.293	6000.567	2	0	2	5	5	0
UltimateEliminator+MathSAT	0	0	32.986	21.228	0	0	0	7	0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3-4.8.17n	0	4	2128.071	2128.256	4	4	0	1	2	1	0
2020-CVC4n	0	1	5370.701	5371.093	1	1	0	4	2	4	0
UltimateEliminator+MathSAT	0	0	23.505	15.586	0	0	0	5	2	0	0
veriT	0	0	4800.321	4800.321	0	0	0	5	2	4	0
smtinterpol	0	0	4800.625	4800.414	0	0	0	5	2	4	0
cvc5	0	0	5816.2	5819.11	0	0	0	5	2	4	0
Vampire	0	0	6000.0	6000.0	0	0	0	5	2	5	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
veriT	0	2	0.024	0.023	2	0	2	0	5	4	0
2020-CVC4n	0	2	0.035	0.034	2	0	2	0	5	4	0
z3-4.8.17n	0	2	0.038	0.035	2	0	2	0	5	1	0
cvc5	0	2	0.046	0.045	2	0	2	0	5	4	0
Vampire	0	2	0.293	0.567	2	0	2	0	5	5	0
smtinterpol	0	2	1.319	0.847	2	0	2	0	5	4	0
UltimateEliminator+MathSAT	0	0	9.482	5.642	0	0	0	2	5	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	4	97.945	97.94	4	2	2	3	3	0
veriT	0	2	96.345	96.344	2	0	2	5	4	0
smtinterpol	0	2	97.944	97.261	2	0	2	5	4	0
2020-CVC4n	0	2	120.035	120.034	2	0	2	5	5	0
cvc5	0	2	120.046	120.045	2	0	2	5	5	0
Vampire	0	2	120.293	120.567	2	0	2	5	5	0
UltimateEliminator+MathSAT	0	0	32.986	21.228	0	0	0	7	0	0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.