LIA (Single Query Track)

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

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

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

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	Timeout	Memout
z3-4.8.17n	0	300	10.819	10.344	300	137	163	0	0	0
cvc5	0	300	78.318	78.213	300	137	163	0	0	0
2021-z3n	0	292	9608.617	9610.012	292	137	155	8	8	0
UltimateEliminator+MathSAT	0	228	95714.771	93819.912	228	72	156	72	72	0
YicesQS	0	182	141132.674	141155.152	182	101	81	118	117	0
Vampire	0	157	172584.806	171862.538	157	3	154	143	143	0
smtinterpol	0	97	130473.89	129603.093	97	8	89	203	100	0
veriT	0	75	24505.539	24482.283	75	0	75	225	19	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	300	10.819	10.344	300	137	163	0	0	0
cvc5	0	300	78.318	78.213	300	137	163	0	0	0
2021-z3n	0	292	9609.617	9609.662	292	137	155	8	8	0
UltimateEliminator+MathSAT	0	230	95788.571	93730.482	230	74	156	70	70	0
YicesQS	0	182	141150.224	141150.252	182	101	81	118	117	0
Vampire	0	157	197786.226	171827.188	157	3	154	143	143	0
smtinterpol	0	97	130473.89	129603.093	97	8	89	203	100	0
veriT	0	75	24507.659	24481.683	75	0	75	225	19	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2021-z3n	0	137	5.457	5.477	137	137	0	0	163	8	0
z3-4.8.17n	0	137	6.089	5.867	137	137	0	0	163	0	0
cvc5	0	137	60.414	60.383	137	137	0	0	163	0	0
YicesQS	0	101	42740.871	42740.899	101	101	0	36	163	117	0
UltimateEliminator+MathSAT	0	74	84098.811	82827.376	74	74	0	63	163	70	0
smtinterpol	0	8	102026.547	101460.228	8	8	0	129	163	100	0
Vampire	0	3	186004.955	160765.929	3	3	0	134	163	143	0
veriT	0	0	1196.067	1186.716	0	0	0	137	163	19	0

UNSAT 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	163	4.731	4.477	163	0	163	0	137	0	0
cvc5	0	163	17.904	17.83	163	0	163	0	137	0	0
UltimateEliminator+MathSAT	0	156	11689.76	10903.106	156	0	156	7	137	70	0
2021-z3n	0	155	9604.16	9604.185	155	0	155	8	137	8	0
Vampire	0	154	11781.272	11061.259	154	0	154	9	137	143	0
smtinterpol	0	89	28447.344	28142.864	89	0	89	74	137	100	0
YicesQS	0	81	98409.353	98409.353	81	0	81	82	137	117	0
veriT	0	75	23311.592	23294.968	75	0	75	88	137	19	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	300	10.819	10.344	300	137	163	0	0	0
cvc5	0	300	78.318	78.213	300	137	163	0	0	0
2021-z3n	0	292	201.617	201.662	292	137	155	8	8	0
UltimateEliminator+MathSAT	0	206	4250.079	3229.435	206	57	149	94	94	0
YicesQS	0	174	3108.924	3108.938	174	93	81	126	125	0
Vampire	0	153	3726.806	3592.231	153	3	150	147	147	0
smtinterpol	0	97	3725.534	3440.239	97	8	89	203	134	0
veriT	0	75	804.494	778.296	75	0	75	225	24	0

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