SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_SLIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 23730
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 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 23626
(base +5) 		18652.40 21584.25 23626 15796 7830 104 0 71 14
Z3-Noodler 0 23622
(base +3231) 		18684.89 21616.10 23622 15791 7831 108 0 72 17
OSTRICH 0 22886 825579.05 544527.98 22901 15192 7709 829 0 829 0
cvc5 0 21585 761359.99 764128.07 21585 14253 7332 2145 0 2139 0
Z3-alpha 0 20333
(base -65) 		298762.46 98595.07 20504 13094 7410 3226 0 2780 146
Z3-Noodler-Mocha-base n 0 23621 19023.35 21928.09 23621 15791 7830 109 0 74 16
Z3-alpha-base n 0 20398 204867.86 207413.21 20398 12933 7465 3332 0 2902 326
Z3-Noodler-base n 0 20391 173430.99 175976.98 20391 12919 7472 3339 0 2914 322
(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 23626
(base +5) 		18652.40 21584.25 23626 15796 7830 104 0 71 14
Z3-Noodler 0 23622
(base +3231) 		18684.89 21616.10 23622 15791 7831 108 0 72 17
OSTRICH 0 22901 850577.80 560592.66 22901 15192 7709 829 0 829 0
cvc5 0 21585 761359.99 764128.07 21585 14253 7332 2145 0 2139 0
Z3-alpha 0 20504
(base +106) 		726625.45 207351.55 20504 13094 7410 3226 0 2780 146
Z3-Noodler-Mocha-base n 0 23621 19023.35 21928.09 23621 15791 7830 109 0 74 16
Z3-alpha-base n 0 20398 204867.86 207413.21 20398 12933 7465 3332 0 2902 326
Z3-Noodler-base n 0 20391 173430.99 175976.98 20391 12919 7472 3339 0 2914 322
(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 15796
(base +5) 		13241.35 15197.64 15796 15796 0 51 7883 46 5
Z3-Noodler 0 15791
(base +2872) 		13270.92 15226.09 15791 15791 0 56 7883 48 8
OSTRICH 0 15192 756376.84 495527.79 15192 15192 0 655 7883 655 0
cvc5 0 14253 689772.73 691621.45 14253 14253 0 1594 7883 1594 0
Z3-alpha 0 13094
(base +161) 		589707.37 170020.57 13094 13094 0 2753 7883 2355 114
Z3-Noodler-Mocha-base n 0 15791 13594.73 15532.38 15791 15791 0 56 7883 49 7
Z3-alpha-base n 0 12933 200771.91 202396.21 12933 12933 0 2914 7883 2518 311
Z3-Noodler-base n 0 12919 169440.71 171059.18 12919 12919 0 2928 7883 2534 312
(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 0 7831
(base +359) 		5413.97 6390.01 7831 0 7831 41 15858 15 7
Z3-Noodler-Mocha 0 7830
(base +0) 		5411.06 6386.61 7830 0 7830 42 15858 16 7
OSTRICH 0 7709 94200.96 65064.87 7709 0 7709 163 15858 163 0
Z3-alpha 0 7410
(base -55) 		136918.08 37330.99 7410 0 7410 462 15858 420 32
cvc5 0 7332 71587.26 72506.63 7332 0 7332 540 15858 534 0
Z3-Noodler-Mocha-base n 0 7830 5428.62 6395.71 7830 0 7830 42 15858 16 7
Z3-Noodler-base n 0 7472 3990.29 4917.80 7472 0 7472 400 15858 375 10
Z3-alpha-base n 0 7465 4095.95 5017.00 7465 0 7465 407 15858 379 15
(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 23575
(base +5) 		7277.51 10201.32 23575 15755 7820 18 137 0 0
Z3-Noodler 0 23568
(base +4301) 		7295.24 10218.22 23568 15748 7820 18 144 0 0
Z3-alpha 0 19545
(base +373) 		83571.56 37652.95 19545 12291 7254 85 4100 0 0
cvc5 0 19286 11147.80 13526.93 19286 12212 7074 6 4438 0 0
OSTRICH 0 18149 153670.82 63582.53 18149 10716 7433 0 5581 0 0
Z3-Noodler-Mocha-base n 0 23570 7386.53 10283.11 23570 15750 7820 18 142 0 0
Z3-Noodler-base n 0 19267 20511.46 22894.70 19267 11828 7439 94 4369 0 0
Z3-alpha-base n 0 19172 20345.60 22711.30 19172 11736 7436 97 4461 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver