QF_UF (Main Track)

Competition results for the QF_UF division as of Fri Oct 30 12:49:29 GMT

Competition benchmarks = 6649
Competition industrial benchmarks = 3

The winners for this division are:

Sequential Performance

Sequential Performance	Sequential Performance (industrial)	Parallel Performance	Parallel Performance (industrial)
Yices	Yices	Yices	Yices

Division COMPLETE

Sequential Performance

Solver	Errors	Corrects	CPU
CVC4	0	6639	44128.25
CVC4 (exp)	0	6639	44166.41
OpenSMT2	0	6629	96687.79
OpenSMT2 (parallel)	2	6537	88233.44
SMT-RAT	1	6629	82780.23
SMTInterpol	0	6568	235333.25
Yices	0	6649	1035.60
MathSatn	0	6571	202950.27
z3n	0	6573	199098.83
veriT	0	6647	7227.04

Sequential Performance (industrial)

Solver	Errors	Corrects	CPU
CVC4	0	3	0.02
CVC4 (exp)	0	3	0.02
OpenSMT2	0	3	0.03
OpenSMT2 (parallel)	0	3	0.03
SMT-RAT	0	3	0.01
SMTInterpol	0	3	0.92
Yices	0	3	0.00
MathSatn	0	3	0.06
z3n	0	3	0.08
veriT	0	3	0.01

Parallel Performance

Solver	Errors	Corrects	CPU	WALL
CVC4	0	6639	44138.17	44132.83
CVC4 (exp)	0	6639	44176.37	44172.88
OpenSMT2	0	6629	96706.70	96655.69
OpenSMT2 (parallel)	2	6541	186019.96	50075.03
SMT-RAT	1	6629	82796.18	82759.84
SMTInterpol	0	6568	589099.08	223141.65
Yices	0	6649	1035.60	1048.25
MathSatn	0	6571	203028.86	202951.80
z3n	0	6573	199169.38	199088.96
veriT	0	6647	7228.97	7233.22

Parallel Performance (industrial)

Solver	Errors	Corrects	CPU	WALL
CVC4	0	3	0.02	0.03
CVC4 (exp)	0	3	0.02	0.03
OpenSMT2	0	3	0.03	0.05
OpenSMT2 (parallel)	0	3	0.03	0.04
SMT-RAT	0	3	0.01	0.03
SMTInterpol	0	3	0.92	0.70
Yices	0	3	0.00	0.02
MathSatn	0	3	0.06	0.06
z3n	0	3	0.08	0.09
veriT	0	3	0.01	0.03

Other Information

Solver	Not Solved	Remaining
CVC4	10	0
CVC4 (exp)	10	0
OpenSMT2	20	0
OpenSMT2 (parallel)	106	0
SMT-RAT	19	0
SMTInterpol	81	0
Yices	0	0
MathSatn	78	0
z3n	76	0
veriT	2	0

n. Non-competitive.