SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NIA (Parallel Track)

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

Results were generated on 2025-08-11

Benchmarks: 44
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 Z3-Parti-Z3pp 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 21 108934.89 1833.83 21 13 8 23 0 23 0
Yices2 0 10 110976.88 878.92 10 4 6 34 0 34 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 44 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
Z3-Parti-Z3pp 0 13 72870.04 1236.13 13 13 0 2 29 2 0
Yices2 0 4 46163.17 366.09 4 4 0 11 29 11 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 15 29 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 15 29 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 15 29 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 8 36064.85 597.70 8 0 8 5 31 5 0
Yices2 0 6 64813.71 512.84 6 0 6 7 31 7 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 13 31 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 13 31 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 13 31 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 9 2292.22 70.28 9 7 2 0 35 0 0
Yices2 0 2 2909.66 24.44 2 0 2 0 42 0 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 44 0 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 44 0 0 0
n: non-competing solver