QF_LIA (Model Validation Track)

Competition results for the QF_LIA logic in the Model Validation Track.

Page generated on 2021-07-18 17:31:50 +0000

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

Winners

Sequential Performance	Parallel Performance
cvc5-mv	cvc5-mv

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
MathSAT5n	0	1830	204232.357	204190.134	80	0
2020-z3n	0	1819	239179.029	239036.978	93	0
cvc5-mv	0	1754	297407.626	297371.91	169	0
z3-mvn	0	1706	364901.925	364851.103	217	0
2020-Yices2-fixed Model Validationn	0	1638	376806.041	376819.762	285	0
2020-Yices2 Model Validationn	0	1638	376813.696	376796.183	285	0
Yices2 model-validation	0	1634	380956.556	380978.7	289	0
SMTInterpol	0	1604	499491.927	479261.96	319	0
OpenSMT	0	1222	871292.562	976940.2	228	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
MathSAT5n	0	1830	204241.777	204187.064	80	0
2020-z3n	0	1819	239192.309	239033.678	93	0
cvc5-mv	0	1754	297421.676	297367.13	169	0
z3-mvn	0	1706	364931.845	364842.353	217	0
2020-Yices2 Model Validationn	0	1638	376836.096	376786.983	285	0
2020-Yices2-fixed Model Validationn	0	1638	376827.861	376810.512	285	0
Yices2 model-validation	0	1634	380977.076	380972.16	289	0
SMTInterpol	0	1605	500189.947	479097.87	318	0
OpenSMT	0	1222	897206.746	976930.21	228	0

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