SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Strings (Single Query Track)

Competition results for the QF_Strings division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

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 34110
(base +521) 		22239.22 26476.54 34110 22093 12017 118 0 75 24
Z3-Noodler 0 33635
(base +4282) 		23260.58 27437.40 33635 22088 11547 593 0 77 29
OSTRICH 0 32766 876070.90 572896.46 32781 21440 11341 1447 0 1447 0
cvc5 0 30671 794564.28 798463.70 30671 20275 10396 3557 0 3532 4
Z3-alpha 0 29350
(base -71) 		319765.74 110490.43 29524 19113 10411 4704 0 3155 213
Z3-Noodler-Mocha-base n 0 33589 23586.42 27719.87 33589 22088 11501 639 0 79 28
Z3-alpha-base n 0 29421 219342.97 223002.50 29421 18963 10458 4807 0 3350 330
Z3-Noodler-base n 0 29353 188202.78 191856.12 29353 18882 10471 4875 0 3354 325
(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 34110
(base +521) 		22239.22 26476.54 34110 22093 12017 118 0 75 24
Z3-Noodler 0 33635
(base +4282) 		23260.58 27437.40 33635 22088 11547 593 0 77 29
OSTRICH 0 32781 901069.65 588961.14 32781 21440 11341 1447 0 1447 0
cvc5 0 30671 794564.28 798463.70 30671 20275 10396 3557 0 3532 4
Z3-alpha 0 29524
(base +103) 		753806.26 220794.86 29524 19113 10411 4704 0 3155 213
Z3-Noodler-Mocha-base n 0 33589 23586.42 27719.87 33589 22088 11501 639 0 79 28
Z3-alpha-base n 0 29421 219342.97 223002.50 29421 18963 10458 4807 0 3350 330
Z3-Noodler-base n 0 29353 188202.78 191856.12 29353 18882 10471 4875 0 3354 325
(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 22093
(base +5) 		15882.66 18623.47 22093 22093 0 51 12084 46 5
Z3-Noodler 0 22088
(base +3206) 		15946.83 18685.22 22088 22088 0 56 12084 48 8
OSTRICH 0 21440 788987.02 514244.86 21440 21440 0 704 12084 704 0
cvc5 0 20275 698596.23 701193.20 20275 20275 0 1869 12084 1851 3
Z3-alpha 0 19113
(base +150) 		603853.08 178234.40 19113 19113 0 3031 12084 2362 128
Z3-Noodler-Mocha-base n 0 22088 16244.80 18958.23 22088 22088 0 56 12084 49 7
Z3-alpha-base n 0 18963 207693.33 210062.17 18963 18963 0 3181 12084 2536 313
Z3-Noodler-base n 0 18882 175609.63 177963.63 18882 18882 0 3262 12084 2551 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-Mocha 0 12017
(base +516) 		6356.56 7853.07 12017 0 12017 46 22165 17 10
Z3-Noodler 0 11547
(base +1076) 		7313.76 8752.18 11547 0 11547 516 22165 17 12
OSTRICH 0 11341 112082.64 74716.29 11341 0 11341 722 22165 722 0
Z3-alpha 0 10411
(base -47) 		149953.18 42560.47 10411 0 10411 1652 22165 778 85
cvc5 0 10396 95968.05 97270.49 10396 0 10396 1667 22165 1660 1
Z3-Noodler-Mocha-base n 0 11501 7341.62 8761.64 11501 0 11501 562 22165 18 12
Z3-Noodler-base n 0 10471 12593.14 13892.50 10471 0 10471 1592 22165 788 13
Z3-alpha-base n 0 10458 11649.63 12940.33 10458 0 10458 1605 22165 799 17
(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 34057
(base +541) 		9685.94 13914.77 34057 22050 12007 18 153 0 0
Z3-Noodler 0 33559
(base +5385) 		9922.05 14087.58 33559 22042 11517 486 183 0 0
Z3-alpha 0 28480
(base +334) 		94402.79 44519.30 28480 18253 10227 1117 4631 0 1
cvc5 0 28267 13626.55 17119.73 28267 18205 10062 20 5941 0 0
OSTRICH 0 27956 190516.66 82017.96 27956 16907 11049 0 6272 0 0
Z3-Noodler-Mocha-base n 0 33516 10023.07 14145.41 33516 22044 11472 531 181 0 0
Z3-Noodler-base n 0 28174 23832.92 27315.09 28174 17763 10411 1187 4867 0 0
Z3-alpha-base n 0 28146 23855.72 27327.91 28146 17740 10406 1120 4962 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver