SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_IDL (Parallel Track)

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

Results were generated on 2025-08-11

Benchmarks: 45
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
- Z3-Parti-Z3pp SMTS Z3-Parti-Z3pp Z3-Parti-Z3pp

Parallel 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 450401.68 7250.13 11 1 10 34 0 34 0
SMTS 0 9 410591.78 3252.19 9 6 3 36 0 36 0
Yices2 0 1 11255.05 88.72 1 1 0 44 0 44 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 45 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 45 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 45 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 45 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 45 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 6 252447.31 1985.76 6 6 0 4 35 4 0
Z3-Parti-Z3pp 0 1 450.98 10.98 1 1 0 9 35 9 0
Yices2 0 1 11255.05 88.72 1 1 0 9 35 9 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 10 35 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 10 35 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 10 35 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 10 35 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 10 35 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 10 449950.70 7239.15 10 0 10 12 23 12 0
SMTS 0 3 158144.47 1266.43 3 0 3 19 23 19 0
Yices2 0 0 0.00 0.00 0 0 0 22 23 22 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 22 23 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 22 23 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 22 23 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 22 23 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 22 23 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
Z3-Parti-Z3pp 0 1 450.98 10.98 1 1 0 0 44 0 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 45 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 45 0 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 45 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 45 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 45 0 0 0
n: non-competing solver