SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NRA (Single Query Track)

Competition results for the QF_NRA logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Z3-alpha Z3-alpha Z3-alpha Z3-alpha Z3-alpha

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 2856
(base +9) 		67264.36 22562.80 2872 1452 1420 232 0 230 1
z3siri 0 2803
(base -44) 		80486.25 80842.87 2803 1413 1390 301 0 295 1
cvc5 0 2766 114285.94 114640.93 2766 1353 1413 338 0 338 0
Yices2 0 2746 21997.19 22341.69 2746 1392 1354 358 0 357 1
SMT-RAT 0 2582 75051.01 75380.36 2582 1296 1286 522 0 521 1
SMTInterpol 0 551 4555.75 3400.39 551 22 529 2553 0 0 0
Z3-alpha-base n 0 2847 50463.53 50822.13 2847 1433 1414 257 0 255 2
z3siri-base n 0 2847 51826.40 52185.55 2847 1433 1414 257 0 255 2
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 2872
(base +25) 		104134.69 33978.73 2872 1452 1420 232 0 230 1
z3siri 0 2803
(base -44) 		80486.25 80842.87 2803 1413 1390 301 0 295 1
cvc5 0 2766 114285.94 114640.93 2766 1353 1413 338 0 338 0
Yices2 0 2746 21997.19 22341.69 2746 1392 1354 358 0 357 1
SMT-RAT 0 2582 75051.01 75380.36 2582 1296 1286 522 0 521 1
SMTInterpol 0 551 4555.75 3400.39 551 22 529 2553 0 0 0
Z3-alpha-base n 0 2847 50463.53 50822.13 2847 1433 1414 257 0 255 2
z3siri-base n 0 2847 51826.40 52185.55 2847 1433 1414 257 0 255 2
(base +/- n): for derived solvers: increment over base solver
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-alpha 0 1452
(base +19) 		45895.54 15216.23 1452 1452 0 88 1564 86 1
z3siri 0 1413
(base -20) 		27290.79 27468.80 1413 1413 0 127 1564 126 0
Yices2 0 1392 13962.43 14137.35 1392 1392 0 148 1564 148 0
cvc5 0 1353 53885.77 54059.48 1353 1353 0 187 1564 187 0
SMT-RAT 0 1296 34785.43 34950.85 1296 1296 0 244 1564 244 0
SMTInterpol 0 22 3267.57 2870.90 22 22 0 1518 1564 0 0
Z3-alpha-base n 0 1433 15586.25 15765.45 1433 1433 0 107 1564 106 1
z3siri-base n 0 1433 16021.22 16200.71 1433 1433 0 107 1564 106 1
(base +/- n): for derived solvers: increment over base solver
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-alpha 0 1420
(base +6) 		58239.15 18762.51 1420 0 1420 37 1647 37 0
cvc5 0 1413 60400.18 60581.46 1413 0 1413 44 1647 44 0
z3siri 0 1390
(base -24) 		53195.46 53374.08 1390 0 1390 67 1647 64 0
Yices2 0 1354 8034.77 8204.34 1354 0 1354 103 1647 102 1
SMT-RAT 0 1286 40265.58 40429.50 1286 0 1286 171 1647 171 0
SMTInterpol 0 529 1288.17 529.49 529 0 529 928 1647 0 0
Z3-alpha-base n 0 1414 34877.29 35056.68 1414 0 1414 43 1647 43 0
z3siri-base n 0 1414 35805.18 35984.83 1414 0 1414 43 1647 43 0
(base +/- n): for derived solvers: increment over base solver
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-alpha 0 2690
(base +293) 		7786.82 3548.56 2690 1390 1300 0 414 0 0
Yices2 0 2633 1777.40 2104.80 2633 1339 1294 0 471 0 0
cvc5 0 2507 2628.03 2937.21 2507 1251 1256 0 597 0 0
SMT-RAT 0 2299 3253.10 3537.32 2299 1195 1104 0 805 0 0
z3siri 0 2256
(base -141) 		1612.73 1891.29 2256 1240 1016 0 848 0 0
SMTInterpol 0 536 1373.30 564.25 536 7 529 2507 61 0 0
z3siri-base n 0 2397 2729.81 3026.06 2397 1333 1064 0 707 0 0
Z3-alpha-base n 0 2397 2744.32 3040.61 2397 1333 1064 0 707 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver