QF_LIRA (Model Validation Track)

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

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

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

Winners

Sequential Performance	Parallel Performance
Yices2 model-validation	Yices2 model-validation

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
2020-Yices2 Model Validationn	0	1	0.117	0.117	0	0
2020-Yices2-fixed Model Validationn	0	1	0.117	0.117	0	0
Yices2 model-validation	0	1	0.118	0.118	0	0
2020-z3n	0	1	0.336	0.336	0	0
z3-mvn	0	1	0.357	0.341	0	0
MathSAT5n	0	1	0.476	0.479	0	0
cvc5-mv	0	1	2.353	2.352	0	0
SMTInterpol	0	1	18.236	6.262	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
2020-Yices2 Model Validationn	0	1	0.117	0.117	0	0
2020-Yices2-fixed Model Validationn	0	1	0.117	0.117	0	0
Yices2 model-validation	0	1	0.118	0.118	0	0
2020-z3n	0	1	0.336	0.336	0	0
z3-mvn	0	1	0.357	0.341	0	0
MathSAT5n	0	1	0.476	0.479	0	0
cvc5-mv	0	1	2.353	2.352	0	0
SMTInterpol	0	1	18.236	6.262	0	0

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