SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFDTLIA (Single Query Track)

Competition results for the AUFDTLIA logic in the Single Query 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)
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 293 22120.50 22159.62 293 85 208 7 0 7 0
SMTInterpol 0 185 1365.83 803.67 185 1 184 115 0 16 0
iProver v3.9.3 0 170 14058.01 3804.33 179 0 179 121 0 112 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 293 22120.50 22159.62 293 85 208 7 0 7 0
SMTInterpol 0 185 1365.83 803.67 185 1 184 115 0 16 0
iProver v3.9.3 0 179 31083.98 8115.91 179 0 179 121 0 112 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 85 22043.88 22057.12 85 85 0 0 215 0 0
SMTInterpol 0 1 0.64 0.55 1 1 0 84 215 11 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 85 215 85 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 208 76.62 102.50 208 0 208 0 92 0 0
SMTInterpol 0 184 1365.20 803.12 184 0 184 24 92 0 0
iProver v3.9.3 0 179 31083.98 8115.91 179 0 179 29 92 20 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 250 90.08 120.93 250 42 208 0 50 0 0
SMTInterpol 0 178 782.42 323.69 178 1 177 89 33 0 0
iProver v3.9.3 0 133 1410.69 484.35 133 0 133 0 167 0 0