QF_LRA (Model Validation Track)

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

Page generated on 2022-08-10 11:19:11 +0000

Benchmarks: 516
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	503	30845.95	30855.664	13	0
z3-4.8.17n	0	493	47161.62	47076.568	23	0
2021-Yices2 model-validationn	0	492	38500.854	38465.45	24	0
Yices2	0	492	38593.063	38601.258	24	0
cvc5	0	490	55737.64	55751.912	26	0
smtinterpol	0	478	81036.342	76749.912	38	0
MathSATn	0	474	69800.441	69815.678	41	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
OpenSMT	0	503	30849.47	30855.164	13	0
z3-4.8.17n	0	493	47165.11	47075.808	23	0
2021-Yices2 model-validationn	0	492	38502.494	38464.71	24	0
Yices2	0	492	38595.663	38600.198	24	0
cvc5	0	490	55744.37	55750.712	26	0
smtinterpol	0	479	81063.062	76719.742	37	0
MathSATn	0	474	69807.621	69813.788	41	0

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