SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LIA (Parallel Track)

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

Results were generated on 2025-08-11

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

Winners

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

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTS 0 19 461737.60 3641.39 19 16 3 25 0 25 0
Z3-Parti-Z3pp 0 12 171004.46 2849.27 12 11 1 32 0 32 0
Yices2 0 3 185242.16 1454.71 3 2 1 41 0 41 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 44 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 44 0 0 0
n: non-competing solver

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTS 0 16 337455.69 2660.60 16 16 0 9 19 9 0
Z3-Parti-Z3pp 0 11 165274.55 2744.19 11 11 0 14 19 14 0
Yices2 0 2 59618.20 469.36 2 2 0 23 19 23 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 25 19 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 25 19 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 25 19 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 25 19 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 25 19 0 0
n: non-competing solver

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTS 0 3 124281.91 980.78 3 0 3 15 26 15 0
Z3-Parti-Z3pp 0 1 5729.91 105.08 1 0 1 17 26 17 0
Yices2 0 1 125623.96 985.35 1 0 1 17 26 17 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 18 26 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 18 26 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 18 26 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 18 26 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 18 26 0 0
n: 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
SMTS 0 5 5617.51 49.26 5 5 0 0 39 0 0
Z3-Parti-Z3pp 0 1 758.71 22.07 1 1 0 0 43 0 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 44 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 44 0 0 0
n: non-competing solver