SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_SNIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 cvc5 cvc5 - cvc5

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 70 11.21 19.96 70 70 0 0 0 0 0
Z3-Noodler 0 70
(base +70) 		11.62 20.43 70 70 0 0 0 0 0
Z3-Noodler-Mocha 0 70
(base +0) 		11.71 20.52 70 70 0 0 0 0 0
Z3-alpha 0 70
(base +0) 		15.28 23.99 70 70 0 0 0 0 0
OSTRICH 0 70 146.75 88.70 70 70 0 0 0 0 0
Z3-Noodler-Mocha-base n 0 70 11.54 20.25 70 70 0 0 0 0 0
Z3-alpha-base n 0 70 12.49 21.19 70 70 0 0 0 0 0
Z3-Noodler-base n 0 0 0.00 0.00 0 0 0 70 0 0 0
(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
cvc5 0 70 11.21 19.96 70 70 0 0 0 0 0
Z3-Noodler 0 70
(base +70) 		11.62 20.43 70 70 0 0 0 0 0
Z3-Noodler-Mocha 0 70
(base +0) 		11.71 20.52 70 70 0 0 0 0 0
Z3-alpha 0 70
(base +0) 		15.28 23.99 70 70 0 0 0 0 0
OSTRICH 0 70 146.75 88.70 70 70 0 0 0 0 0
Z3-Noodler-Mocha-base n 0 70 11.54 20.25 70 70 0 0 0 0 0
Z3-alpha-base n 0 70 12.49 21.19 70 70 0 0 0 0 0
Z3-Noodler-base n 0 0 0.00 0.00 0 0 0 70 0 0 0
(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
cvc5 0 70 11.21 19.96 70 70 0 0 0 0 0
Z3-Noodler 0 70
(base +70) 		11.62 20.43 70 70 0 0 0 0 0
Z3-Noodler-Mocha 0 70
(base +0) 		11.71 20.52 70 70 0 0 0 0 0
Z3-alpha 0 70
(base +0) 		15.28 23.99 70 70 0 0 0 0 0
OSTRICH 0 70 146.75 88.70 70 70 0 0 0 0 0
Z3-Noodler-Mocha-base n 0 70 11.54 20.25 70 70 0 0 0 0 0
Z3-alpha-base n 0 70 12.49 21.19 70 70 0 0 0 0 0
Z3-Noodler-base n 0 0 0.00 0.00 0 0 0 70 0 0 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
cvc5 0 70 11.21 19.96 70 70 0 0 0 0 0
Z3-Noodler 0 70
(base +70) 		11.62 20.43 70 70 0 0 0 0 0
Z3-Noodler-Mocha 0 70
(base +0) 		11.71 20.52 70 70 0 0 0 0 0
Z3-alpha 0 70
(base +0) 		15.28 23.99 70 70 0 0 0 0 0
OSTRICH 0 70 146.75 88.70 70 70 0 0 0 0 0
Z3-Noodler-Mocha-base n 0 70 11.54 20.25 70 70 0 0 0 0 0
Z3-alpha-base n 0 70 12.49 21.19 70 70 0 0 0 0 0
Z3-Noodler-base n 0 0 0.00 0.00 0 0 0 70 0 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver