QF_LIA (Model Validation Track)

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

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

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

Winners

Sequential Performance	Parallel Performance
Z3++	Z3++

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
Z3++	0	4078	223671.692	224739.043	106	6
2020-z3n	0	4073	272161.825	272055.953	108	2
MathSATn	0	4050	266606.64	266561.143	132	0
z3-4.8.17n	0	4032	284918.865	284670.43	162	2
OpenSMT	0	3994	477436.125	477337.742	201	0
cvc5	0	3992	352537.004	352478.219	203	0
Yices2	0	3905	408746.205	408736.121	291	0
smtinterpol	0	3814	600133.529	575944.074	382	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Timeout	Memout
Z3++	0	4078	223688.172	224734.873	106	6
2020-z3n	0	4073	272179.315	272050.813	108	2
MathSATn	0	4050	266622.02	266555.603	132	0
z3-4.8.17n	0	4032	284933.215	284664.68	162	2
OpenSMT	0	3994	477456.615	477330.582	201	0
cvc5	0	3992	352563.424	352470.659	203	0
Yices2	0	3905	408770.615	408727.321	291	0
smtinterpol	0	3814	600133.529	575944.074	382	0

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