QF_LinearIntArith (Parallel Track)
Competition results for the QF_LinearIntArith
division
in the Parallel Track. Chart
Results were generated on 2025-08-11
Benchmarks: 89
Time Limit: 1200 seconds
Memory Limit: 30720 GB
Logics:Winners
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|
| - | SMTS | SMTS | Z3-Parti-Z3pp | 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 | 28 | 872329.38 | 6893.58 | 28 | 22 | 6 | 61 | 0 | 61 | 0 |
| Z3-Parti-Z3pp | 0 | 23 | 621406.13 | 10099.40 | 23 | 12 | 11 | 66 | 0 | 66 | 0 |
| Yices2 | 0 | 4 | 196497.21 | 1543.43 | 4 | 3 | 1 | 85 | 0 | 85 | 0 |
| SMTS (32 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| SMTS (64 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| Z3-Parti-Z3pp-16core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| Z3-Parti-Z3pp-32core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| Z3-Parti-Z3pp-64core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 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 | 22 | 589903.00 | 4646.37 | 22 | 22 | 0 | 13 | 54 | 13 | 0 |
| Z3-Parti-Z3pp | 0 | 12 | 165725.53 | 2755.17 | 12 | 12 | 0 | 23 | 54 | 23 | 0 |
| Yices2 | 0 | 3 | 70873.25 | 558.08 | 3 | 3 | 0 | 32 | 54 | 32 | 0 |
| SMTS (32 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 35 | 54 | 0 | 0 |
| SMTS (64 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 35 | 54 | 0 | 0 |
| Z3-Parti-Z3pp-16core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 35 | 54 | 0 | 0 |
| Z3-Parti-Z3pp-32core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 35 | 54 | 0 | 0 |
| Z3-Parti-Z3pp-64core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 35 | 54 | 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 |
|---|
| Z3-Parti-Z3pp | 0 | 11 | 455680.60 | 7344.23 | 11 | 0 | 11 | 29 | 49 | 29 | 0 |
| SMTS | 0 | 6 | 282426.39 | 2247.21 | 6 | 0 | 6 | 34 | 49 | 34 | 0 |
| Yices2 | 0 | 1 | 125623.96 | 985.35 | 1 | 0 | 1 | 39 | 49 | 39 | 0 |
| SMTS (32 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 40 | 49 | 0 | 0 |
| SMTS (64 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 40 | 49 | 0 | 0 |
| Z3-Parti-Z3pp-16core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 40 | 49 | 0 | 0 |
| Z3-Parti-Z3pp-32core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 40 | 49 | 0 | 0 |
| Z3-Parti-Z3pp-64core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 40 | 49 | 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 | 84 | 0 | 0 |
| Z3-Parti-Z3pp | 0 | 2 | 1209.69 | 33.05 | 2 | 2 | 0 | 0 | 87 | 0 | 0 |
| SMTS (32 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| SMTS (64 cores) n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| Z3-Parti-Z3pp-16core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| Z3-Parti-Z3pp-32core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
| Z3-Parti-Z3pp-64core n | 0 | 0 | 0.00 | 0.00 | 0 | 0 | 0 | 89 | 0 | 0 | 0 |
n: non-competing solver