QF_Equality_LinearArith (Parallel Track)

Competition results for the QF_Equality_LinearArith division in the Parallel Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_ALIA : 6 benchmarks
QF_UFIDL : 38 benchmarks
QF_UFLIA : 27 benchmarks
QF_UFLRA : 6 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
-	z3-parallel	z3-parallel	z3-parallel	-

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
z3-parallel	18	361914.41	5377.36	18	13	5	59	59
OpenSMT-SMTS ^ne	6 (base -6)	312390.48	2462.32	6	3	3	71	67
OpenSMT-SMTS-base ⁿ	12	8589.01	8591.89	12	1	11	65	65

(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

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-parallel	13	223259.93	3465.51	13	13	4	60	4
OpenSMT-SMTS ^ne	3 (base +2)	151969.69	1196.21	3	3	14	60	14
OpenSMT-SMTS-base ⁿ	1	211.43	211.58	1	1	16	60	16

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
z3-parallel	5	138654.48	1911.85	5	5	35	37	35
OpenSMT-SMTS ^ne	3 (base -8)	160420.79	1266.11	3	3	37	37	33
OpenSMT-SMTS-base ⁿ	11	8377.57	8380.31	11	11	29	37	29