LRA (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
YicesQS	0	1003	413.503	413.789	1003	408	595	0	0	0
2021-z3n	0	948	107064.15	107064.882	948	387	561	55	55	0
z3-4.8.17n	0	936	121636.013	121630.935	936	378	558	67	67	0
UltimateEliminator+MathSAT	0	847	203336.187	199665.048	847	327	520	156	156	0
cvc5	0	834	223869.247	224000.623	834	344	490	169	169	0
Vampire	0	484	663805.469	629596.558	484	0	484	519	515	0
smtinterpol	0	164	55535.315	51526.051	164	1	163	839	36	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
YicesQS	0	1003	413.503	413.789	1003	408	595	0	0	0
2021-z3n	0	948	107068.47	107063.302	948	387	561	55	55	0
z3-4.8.17n	0	936	121640.083	121628.735	936	378	558	67	67	0
UltimateEliminator+MathSAT	0	847	203336.187	199665.048	847	327	520	156	156	0
cvc5	0	834	223996.817	223992.503	834	344	490	169	169	0
Vampire	0	484	746608.829	629466.798	484	0	484	519	515	0
smtinterpol	0	164	55535.315	51526.051	164	1	163	839	36	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
YicesQS	0	408	335.014	335.156	408	408	0	0	595	0	0
2021-z3n	0	387	32756.303	32757.062	387	387	0	21	595	55	0
z3-4.8.17n	0	378	44177.991	44175.707	378	378	0	30	595	67	0
cvc5	0	344	81340.166	81322.414	344	344	0	64	595	169	0
UltimateEliminator+MathSAT	0	327	103826.696	102284.603	327	327	0	81	595	156	0
smtinterpol	0	1	38376.578	36772.9	1	1	0	407	595	36	0
Vampire	0	0	547202.14	489496.77	0	0	0	408	595	515	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
YicesQS	0	595	78.489	78.634	595	0	595	0	408	0	0
2021-z3n	0	561	74312.167	74306.24	561	0	561	34	408	55	0
z3-4.8.17n	0	558	77462.091	77453.028	558	0	558	37	408	67	0
UltimateEliminator+MathSAT	0	520	99509.491	97380.445	520	0	520	75	408	156	0
cvc5	0	490	142656.651	142670.089	490	0	490	105	408	169	0
Vampire	0	484	199406.689	139970.028	484	0	484	111	408	515	0
smtinterpol	0	163	17158.737	14753.151	163	0	163	432	408	36	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
YicesQS	0	1001	174.252	174.481	1001	406	595	2	2	0
2021-z3n	0	835	5387.639	5378.442	835	364	471	168	168	0
z3-4.8.17n	0	823	5521.172	5506.703	823	354	469	180	180	0
UltimateEliminator+MathSAT	0	808	10518.962	7716.21	808	314	494	195	195	0
cvc5	0	719	7344.669	7335.9	719	294	425	284	284	0
Vampire	0	221	19847.831	19055.48	221	0	221	782	781	0
smtinterpol	0	158	6391.051	3350.33	158	1	157	845	66	0

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