QF_LinearRealArith (Model Validation Track)

Competition results for the QF_LinearRealArith division in the Model Validation Track.

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

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

Logics:

• QF_RDL : 109 benchmarks
• QF_LRA : 473 benchmarks

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Yices2 model-validation	0	567	26930.238	26925.162		15	0
OpenSMT	0	564	38606.715	38619.528		18	0
z3-mvn	0	563	49212.205	49211.363		19	0
2020-Yices2-fixed Model Validationn	0	560	32928.827	32933.084		22	0
cvc5-mv	0	559	51828.804	51822.55		23	0
SMTInterpol	0	543	88370.549	83470.299		39	0
MathSAT5n	0	539	70236.873	70254.254		39	0
2020-OpenSMTn	0	464	23505.938	23482.55		9	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Yices2 model-validation	0	567	26931.908	26924.602		15	0
OpenSMT	0	564	38608.125	38618.968		18	0
z3-mvn	0	563	49214.765	49210.393		19	0
2020-Yices2-fixed Model Validationn	0	560	32931.437	32932.294		22	0
cvc5-mv	0	559	51832.764	51821.75		23	0
SMTInterpol	0	543	88370.549	83470.299		39	0
MathSAT5n	0	539	70244.593	70252.644		39	0
2020-OpenSMTn	0	464	23506.708	23482.28		9	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.