SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LRA (Parallel Track)

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

Results were generated on 2025-08-11

Benchmarks: 38
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 21 719350.42 5789.04 21 13 8 17 0 17 0
Yices2 0 12 758621.19 5956.30 12 9 3 26 0 26 0
Z3-Parti-Z3pp 0 7 300574.48 5076.01 7 4 3 31 0 31 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 38 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 38 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 38 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 38 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 38 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 20 5 0
Yices2 0 9 680595.95 5342.44 9 9 0 9 20 9 0
Z3-Parti-Z3pp 0 4 168231.80 2961.30 4 4 0 14 20 14 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 18 20 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 18 20 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 18 20 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 18 20 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 18 20 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 8 140594.21 1177.06 8 0 8 8 22 8 0
Yices2 0 3 78025.24 613.86 3 0 3 13 22 13 0
Z3-Parti-Z3pp 0 3 132342.67 2114.71 3 0 3 13 22 13 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 16 22 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 16 22 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 16 22 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 16 22 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 16 22 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 37 0 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 38 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 38 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 38 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 38 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 38 0 0 0
n: non-competing solver