QF_LRA (Model Validation Track)

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

Page generated on 2020-07-04 11:50:14 +0000

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

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
OpenSMT	0	366	23196.707	23147.053		12	0
Yices2 Model Validation	0	361	27231.252	27220.592		17	0
Yices2-fixed Model Validationn	0	361	27293.683	27273.164		17	0
z3n	0	361	30902.311	30890.314		17	0
CVC4-mv	0	360	36177.219	36183.088		18	0
SMTInterpol-fixedn	0	351	54948.511	52217.779		27	0
SMTInterpol	2*	350	54559.699	51766.013		26	0
MathSAT5-mvn	2*	345	53776.173	53764.771		31	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
OpenSMT	0	366	23197.627	23146.593		12	0
Yices2 Model Validation	0	361	27233.072	27220.212		17	0
Yices2-fixed Model Validationn	0	361	27294.953	27272.744		17	0
z3n	0	361	30904.961	30889.864		17	0
CVC4-mv	0	360	36181.659	36182.578		18	0
SMTInterpol-fixedn	0	351	54948.511	52217.779		27	0
SMTInterpol	2*	350	54559.699	51766.013		26	0
MathSAT5-mvn	2*	345	53783.173	53763.351		31	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.
* The error score is caused by SMTInterpol giving values to defined functions (syntactic problems). It does not indicate an unsoundness.
* The error score is caused by MathSAT not giving full models (syntactic problems). It does not indicate an unsoundness.