QF_LRA (Model Validation Track)

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

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

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

Winners

Sequential Performance	Parallel Performance
OpenSMT	OpenSMT

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
OpenSMT	0	464	22434.98	22445.746	9	0
2020-OpenSMTn	0	464	23505.938	23482.55	9	0
z3-mvn	0	459	38429.569	38431.174	14	0
Yices2 model-validation	0	458	26127.284	26123.621	15	0
cvc5-mv	0	452	45547.164	45539.696	21	0
2020-Yices2-fixed Model Validationn	0	451	32123.88	32129.069	22	0
SMTInterpol	0	440	74196.746	70327.337	33	0
MathSAT5n	0	432	63460.823	63477.111	37	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
OpenSMT	0	464	22435.87	22445.486	9	0
2020-OpenSMTn	0	464	23506.708	23482.28	9	0
z3-mvn	0	459	38431.759	38430.484	14	0
Yices2 model-validation	0	458	26128.954	26123.061	15	0
cvc5-mv	0	452	45550.944	45539.016	21	0
2020-Yices2-fixed Model Validationn	0	451	32126.49	32128.279	22	0
SMTInterpol	0	440	74196.746	70327.337	33	0
MathSAT5n	0	432	63468.273	63475.641	37	0

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