SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LinearRealArith (Parallel Track)

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

Results were generated on 2025-08-11

Benchmarks: 62
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 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 22 833624.72 6755.38 22 13 9 40 0 40 0
Yices2 0 13 871843.19 6848.20 13 9 4 49 0 49 0
Z3-Parti-Z3pp 0 8 370646.06 6193.52 8 4 4 54 0 54 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 62 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 62 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 62 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 62 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 62 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 13 578756.20 4611.98 13 13 0 5 44 5 0
Yices2 0 9 680595.95 5342.44 9 9 0 9 44 9 0
Z3-Parti-Z3pp 0 4 168231.80 2961.30 4 4 0 14 44 14 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 18 44 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 18 44 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 18 44 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 18 44 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 18 44 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 9 254868.52 2143.40 9 0 9 9 44 9 0
Yices2 0 4 191247.24 1505.76 4 0 4 14 44 14 0
Z3-Parti-Z3pp 0 4 202414.26 3232.23 4 0 4 14 44 14 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 18 44 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 18 44 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 18 44 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 18 44 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 18 44 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 1 2160.24 18.12 1 1 0 0 61 0 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 62 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 62 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 62 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 62 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 62 0 0 0
n: non-competing solver