QF_NonLinearRealArith (Model Validation Track)

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

Page generated on 2023-07-06 16:06:00 +0000

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

Logics:

• QF_NRA : 2982 benchmarks

This division is experimental. Solvers are only ranked by performance, but no winner is selected.

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Z3++	0	2803	26911.81	26806.307		85	0
SMT-RAT-MCSAT	0	2605	28708.129	28705.332		256	3
Yices2	0	2172	13928.772	13920.287		239	0
cvc5	0	2111	35969.615	35914.853		237	0
cvc5-NRA-LS	0	2107	34103.514	34109.773		4	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Z3++	0	2803	26911.81	26806.307		85	0
SMT-RAT-MCSAT	0	2605	28708.129	28705.332		256	3
Yices2	0	2172	13928.772	13920.287		239	0
cvc5	0	2111	35969.615	35914.853		237	0
cvc5-NRA-LS	0	2107	34103.514	34109.773		4	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.