QF_Equality+LinearArith (Model Validation Track)

Competition results for the QF_Equality+LinearArith division in the Model Validation Track.

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

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

Logics:

• QF_UFIDL : 206 benchmarks
• QF_UFLIA : 330 benchmarks
• QF_UFLRA : 385 benchmarks

Winners

Sequential Performance	Parallel Performance
SMTInterpol	SMTInterpol

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
2022-smtinterpoln	0	909	20222.626	15663.037		12	0
SMTInterpol	0	895	25487.104	21160.72		26	0
OpenSMT	0	893	12161.31	12156.124		28	0
cvc5	0	870	30144.941	30148.711		51	0
Yices2	0	844	20388.98	20392.097		77	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
2022-smtinterpoln	0	910	21438.566	16805.957		11	0
SMTInterpol	0	896	26728.824	22334.61		25	0
OpenSMT	0	893	12161.31	12156.124		28	0
cvc5	0	870	30144.941	30148.711		51	0
Yices2	0	844	20388.98	20392.097		77	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.