SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NRA (Parallel Track)

Competition results for the QF_NRA 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 Yices2 Yices2

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 16 265026.04 4296.42 16 12 4 28 0 28 0
Yices2 0 7 6040.43 51.47 7 3 4 37 0 37 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 12 162053.02 2649.77 12 12 0 10 22 10 0
Yices2 0 3 1149.54 10.82 3 3 0 19 22 19 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 22 22 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 22 22 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 22 22 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
Yices2 0 4 4890.88 40.65 4 0 4 1 39 1 0
Z3-Parti-Z3pp 0 4 102973.02 1646.65 4 0 4 1 39 1 0
Z3-Parti-Z3pp-16core n 0 0 0.00 0.00 0 0 0 5 39 0 0
Z3-Parti-Z3pp-32core n 0 0 0.00 0.00 0 0 0 5 39 0 0
Z3-Parti-Z3pp-64core n 0 0 0.00 0.00 0 0 0 5 39 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
Yices2 0 6 2869.12 26.09 6 3 3 0 38 0 0
Z3-Parti-Z3pp 0 5 218.02 29.80 5 4 1 0 39 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