SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Datatypes (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

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

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 332 80124.05 80175.55 332 137 195 220 0 220 0
SMTInterpol 0 194 31652.88 21838.44 195 46 149 357 0 327 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 332 80124.05 80175.55 332 137 195 220 0 220 0
SMTInterpol 0 195 32866.26 23018.30 195 46 149 357 0 327 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 137 16437.24 16456.65 137 137 0 25 390 25 0
SMTInterpol 0 46 10297.99 9696.23 46 46 0 116 390 116 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 195 63686.82 63718.90 195 0 195 92 265 92 0
SMTInterpol 0 149 22568.28 13322.07 149 0 149 138 265 112 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
SMTInterpol 0 117 1031.62 502.14 117 16 101 0 435 0 0
cvc5 0 102 485.80 498.39 102 35 67 0 450 0 0