QF_UFLIA (Single Query Track)

Competition results for the QF_UFLIA 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
2018-Yicesn	0	300	30.625	30.764	300	233	67	0		0	0
Yices 2.6.2	0	300	31.352	31.571	300	233	67	0		0	0
Z3n	0	300	65.623	65.636	300	233	67	0		0	0
CVC4	0	300	318.094	318.147	300	233	67	0		0	0
SMTInterpol	0	300	1122.714	574.57	300	233	67	0		0	0
veriT	0	262	48831.396	48784.442	262	195	67	38		6	0
Alt-Ergo	0	64	179239.217	175841.704	64	0	64	236		62	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	30.625	30.764	300	233	67	0		0	0
Yices 2.6.2	0	300	31.352	31.571	300	233	67	0		0	0
Z3n	0	300	65.623	65.636	300	233	67	0		0	0
CVC4	0	300	318.094	318.147	300	233	67	0		0	0
SMTInterpol	0	300	1122.714	574.57	300	233	67	0		0	0
veriT	0	262	48832.036	48784.182	262	195	67	38		6	0
Alt-Ergo	0	65	180660.337	174403.581	65	0	65	235		61	0

SAT 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	233	6.049	6.189	233	233	0	67	0	0
2018-Yicesn	0	233	6.144	6.226	233	233	0	67	0	0
Z3n	0	233	46.236	46.248	233	233	0	67	0	0
CVC4	0	233	107.235	107.28	233	233	0	67	0	0
SMTInterpol	0	233	788.13	365.892	233	233	0	67	0	0
veriT	0	195	45400.385	45352.236	195	195	0	105	6	0
Alt-Ergo	0	0	169962.705	168111.836	0	0	0	300	61	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Z3n	0	67	19.386	19.388	67	0	67	233	0	0
2018-Yicesn	0	67	24.481	24.538	67	0	67	233	0	0
Yices 2.6.2	0	67	25.303	25.382	67	0	67	233	0	0
SMTInterpol	0	67	334.585	208.678	67	0	67	233	0	0
CVC4	0	67	210.859	210.867	67	0	67	233	0	0
veriT	0	67	3431.651	3431.946	67	0	67	233	6	0
Alt-Ergo	0	65	10697.632	6291.745	65	0	65	235	61	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	30.625	30.764	300	233	67	0		0	0
Yices 2.6.2	0	300	31.352	31.571	300	233	67	0		0	0
Z3n	0	300	65.623	65.636	300	233	67	0		0	0
CVC4	0	297	256.833	256.867	297	233	64	3		3	0
SMTInterpol	0	297	924.242	421.741	297	232	65	3		3	0
veriT	0	169	3965.714	3965.711	169	116	53	131		123	0
Alt-Ergo	0	62	4737.998	3620.514	62	0	62	238		123	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.