SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_S (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-Noodler-Mocha 0 10414
(base +516) 		3575.11 4871.77 10414 6227 4187 14 0 4 10
Z3-Noodler 0 9943
(base +981) 		4564.08 5800.87 9943 6227 3716 485 0 5 12
OSTRICH 0 9810 50345.10 28279.78 9810 6178 3632 618 0 618 0
cvc5 0 9016 33193.09 34315.66 9016 5952 3064 1412 0 1393 4
Z3-alpha 0 8947
(base -6) 		20988.00 11871.38 8950 5949 3001 1478 0 375 67
Z3-Noodler-Mocha-base n 0 9898 4551.53 5771.52 9898 6227 3671 530 0 5 12
Z3-Noodler-base n 0 8962 14771.78 15879.14 8962 5963 2999 1466 0 440 3
Z3-alpha-base n 0 8953 14462.61 15568.10 8953 5960 2993 1475 0 448 4
(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-Noodler-Mocha 0 10414
(base +516) 		3575.11 4871.77 10414 6227 4187 14 0 4 10
Z3-Noodler 0 9943
(base +981) 		4564.08 5800.87 9943 6227 3716 485 0 5 12
OSTRICH 0 9810 50345.10 28279.78 9810 6178 3632 618 0 618 0
cvc5 0 9016 33193.09 34315.66 9016 5952 3064 1412 0 1393 4
Z3-alpha 0 8950
(base -3) 		27165.54 13419.32 8950 5949 3001 1478 0 375 67
Z3-Noodler-Mocha-base n 0 9898 4551.53 5771.52 9898 6227 3671 530 0 5 12
Z3-Noodler-base n 0 8962 14771.78 15879.14 8962 5963 2999 1466 0 440 3
Z3-alpha-base n 0 8953 14462.61 15568.10 8953 5960 2993 1475 0 448 4
(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-Noodler-Mocha 0 6227
(base +0) 		2629.61 3405.30 6227 6227 0 0 4201 0 0
Z3-Noodler 0 6227
(base +264) 		2664.29 3438.70 6227 6227 0 0 4201 0 0
OSTRICH 0 6178 32463.42 18628.36 6178 6178 0 49 4201 49 0
cvc5 0 5952 8812.30 9551.79 5952 5952 0 275 4201 257 3
Z3-alpha 0 5949
(base -11) 		14130.43 8189.85 5949 5949 0 278 4201 7 14
Z3-Noodler-Mocha-base n 0 6227 2638.53 3405.60 6227 6227 0 0 4201 0 0
Z3-Noodler-base n 0 5963 6168.93 6904.44 5963 5963 0 264 4201 17 0
Z3-alpha-base n 0 5960 6908.93 7644.77 5960 5960 0 267 4201 18 2
(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-Noodler-Mocha 0 4187
(base +516) 		945.50 1466.46 4187 0 4187 4 6237 1 3
Z3-Noodler 0 3716
(base +717) 		1899.79 2362.17 3716 0 3716 475 6237 2 5
OSTRICH 0 3632 17881.68 9651.42 3632 0 3632 559 6237 559 0
cvc5 0 3064 24380.79 24763.87 3064 0 3064 1127 6237 1126 1
Z3-alpha 0 3001
(base +8) 		13035.10 5229.48 3001 0 3001 1190 6237 358 53
Z3-Noodler-Mocha-base n 0 3671 1913.00 2365.92 3671 0 3671 520 6237 2 5
Z3-Noodler-base n 0 2999 8602.86 8974.70 2999 0 2999 1192 6237 413 3
Z3-alpha-base n 0 2993 7553.69 7923.33 2993 0 2993 1198 6237 420 2
(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-Noodler-Mocha 0 10412
(base +536) 		2396.72 3692.93 10412 6225 4187 0 16 0 0
Z3-Noodler 0 9921
(base +1014) 		2615.19 3848.93 9921 6224 3697 468 39 0 0
OSTRICH 0 9737 36699.09 18346.72 9737 6121 3616 0 691 0 0
cvc5 0 8911 2467.54 3572.83 8911 5923 2988 14 1503 0 0
Z3-alpha 0 8865
(base -39) 		10815.95 6842.36 8865 5892 2973 1032 531 0 1
Z3-Noodler-Mocha-base n 0 9876 2625.00 3842.05 9876 6224 3652 513 39 0 0
Z3-Noodler-base n 0 8907 3321.46 4420.39 8907 5935 2972 1023 498 0 0
Z3-alpha-base n 0 8904 3497.63 4595.42 8904 5934 2970 1023 501 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver