QF_AX (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices 2.6.2	Yices 2.6.2	Yices 2.6.2	Yices 2.6.2	Yices 2.6.2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices 2.6.2	0	300	4.146	4.814	300	150	150	0		0	0
2018-Yicesn	0	300	4.254	4.805	300	150	150	0		0	0
Z3n	0	300	25.783	25.793	300	150	150	0		0	0
CVC4	0	300	71.28	71.223	300	150	150	0		0	0
SMTInterpol	0	300	401.031	181.983	300	150	150	0		0	0
Alt-Ergo	0	138	55759.336	35948.001	138	0	138	162		12	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2018-Yicesn	0	300	4.254	4.805	300	150	150	0		0	0
Yices 2.6.2	0	300	4.146	4.814	300	150	150	0		0	0
Z3n	0	300	25.783	25.793	300	150	150	0		0	0
CVC4	0	300	71.28	71.223	300	150	150	0		0	0
SMTInterpol	0	300	401.031	181.983	300	150	150	0		0	0
Alt-Ergo	0	147	82680.986	26565.759	147	0	147	153		3	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2018-Yicesn	0	150	1.246	1.597	150	150	0	150	0	0
Yices 2.6.2	0	150	1.199	1.632	150	150	0	150	0	0
CVC4	0	150	8.203	8.165	150	150	0	150	0	0
Z3n	0	150	9.113	9.121	150	150	0	150	0	0
SMTInterpol	0	150	112.675	60.141	150	150	0	150	0	0
Alt-Ergo	0	0	4348.359	1447.184	0	0	0	300	3	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices 2.6.2	0	150	2.947	3.182	150	0	150	150	0	0
2018-Yicesn	0	150	3.008	3.208	150	0	150	150	0	0
Z3n	0	150	16.67	16.672	150	0	150	150	0	0
CVC4	0	150	63.078	63.058	150	0	150	150	0	0
SMTInterpol	0	150	288.356	121.842	150	0	150	150	0	0
Alt-Ergo	0	147	78332.628	25118.575	147	0	147	153	3	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2018-Yicesn	0	300	4.254	4.805	300	150	150	0		0	0
Yices 2.6.2	0	300	4.146	4.814	300	150	150	0		0	0
Z3n	0	300	25.783	25.793	300	150	150	0		0	0
CVC4	0	300	71.28	71.223	300	150	150	0		0	0
SMTInterpol	0	300	401.031	181.983	300	150	150	0		0	0
Alt-Ergo	0	99	3802.304	2361.333	99	0	99	201		76	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.