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 solverSAT 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 solverUNSAT 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 solver24 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