SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

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 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 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 solver

UNSAT 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 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 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