QF_LIA (Parallel Track)

Competition results for the QF_LIA logic in the Parallel Track. Chart

Results were generated on 2026-07-25

Benchmarks: 51
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
-	OpenSMT-SMTS	OpenSMT-SMTS	QiuQi	OpenSMT-SMTS

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
OpenSMT-SMTS	22 (base +15)	507020.93	3999.00	22	22	0	29	29
QiuQi	11	26673.81	2652.23	11	4	7	40	40
z3-parallel	11	521641.48	5042.74	11	11	0	40	40
OpenSMT-SMTS-base ⁿ	7	2022.25	2023.54	7	7	0	44	44

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
OpenSMT-SMTS	22 (base +15)	507020.93	3999.00	22	22	8	21	8
z3-parallel	11	521641.48	5042.74	11	11	19	21	19
QiuQi	4	19703.00	1240.45	4	4	26	21	26
OpenSMT-SMTS-base ⁿ	7	2022.25	2023.54	7	7	23	21	23

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
QiuQi	7	6970.81	1411.78	7	7	12	32	12
OpenSMT-SMTS ^ne	0 (base +0)	0.00	0.00	0	0	19	32	19
z3-parallel	0	0.00	0.00	0	0	19	32	19
OpenSMT-SMTS-base ⁿ	0	0.00	0.00	0	0	19	32	19

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT-SMTS	0	3	4948.31	41.27	3	3	0	0	48	0	0
QiuQi	0	2	105.03	23.72	2	1	1	0	49	0	0

SMT-COMP 2026