SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

ABV (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 2487
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 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 1315 77582.30 77754.86 1315 812 503 1172 0 448 0
UltimateEliminator+MathSAT 0 365 1631.33 766.94 365 278 87 2122 0 1 0
SMTInterpol 0 356 3910.68 2927.10 356 47 309 2131 0 212 0
Bitwuzla 0 215 568.81 595.55 215 188 27 2272 0 86 0

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 1315 77582.30 77754.86 1315 812 503 1172 0 448 0
UltimateEliminator+MathSAT 0 365 1631.33 766.94 365 278 87 2122 0 1 0
SMTInterpol 0 356 3910.68 2927.10 356 47 309 2131 0 212 0
Bitwuzla 0 215 568.81 595.55 215 188 27 2272 0 86 0

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 812 29398.73 29502.66 812 812 0 108 1567 39 0
UltimateEliminator+MathSAT 0 278 1221.10 574.68 278 278 0 642 1567 1 0
Bitwuzla 0 188 30.21 53.52 188 188 0 732 1567 30 0
SMTInterpol 0 47 31.49 25.55 47 47 0 873 1567 64 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 503 48183.58 48252.21 503 0 503 20 1964 20 0
SMTInterpol 0 309 3879.19 2901.55 309 0 309 214 1964 45 0
UltimateEliminator+MathSAT 0 87 410.23 192.27 87 0 87 436 1964 0 0
Bitwuzla 0 27 538.60 542.02 27 0 27 496 1964 6 0

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 713 369.03 456.65 713 490 223 16 1758 0 0
UltimateEliminator+MathSAT 0 365 1631.33 766.94 365 278 87 2119 3 0 0
SMTInterpol 0 345 456.45 290.61 345 47 298 1785 357 0 0
Bitwuzla 0 213 34.72 61.12 213 188 25 2185 89 0 0