SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

ABV (Unsat Core Track)

Competition results for the ABV logic in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 794 3580.54 2661.50 282 282 18 0 9 0
cvc5 0 394 27100.13 27141.82 299 299 1 0 1 0
Bitwuzla 0 112 11.19 14.90 29 29 271 0 3 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 300 0 0 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 794 3580.54 2661.50 282 282 18 0 9 0
cvc5 0 394 27100.13 27141.82 299 299 1 0 1 0
Bitwuzla 0 112 11.19 14.90 29 29 271 0 3 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 300 0 0 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 794 3580.54 2661.50 282 282 18 0 9 0
cvc5 0 394 27100.13 27141.82 299 299 1 0 1 0
Bitwuzla 0 112 11.19 14.90 29 29 271 0 3 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 300 0 0 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 757 398.82 250.46 273 273 8 19 0 0
cvc5 0 229 53.21 67.63 116 116 0 184 0 0
Bitwuzla 0 112 11.19 14.90 29 29 268 3 0 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 300 0 0 0