SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFDTLIRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 4721
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 4158 3033.67 3548.47 4158 0 4158 563 0 557 1
iProver v3.9.3 0 3595 161081.52 44682.69 3749 0 3749 972 0 972 0
SMTInterpol 0 3398 21257.74 13583.58 3398 0 3398 1323 0 1148 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 4158 3033.67 3548.47 4158 0 4158 563 0 557 1
iProver v3.9.3 0 3749 560108.14 145624.41 3749 0 3749 972 0 972 0
SMTInterpol 0 3398 21257.74 13583.58 3398 0 3398 1323 0 1148 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 4158 3033.67 3548.47 4158 0 4158 1 562 1 0
iProver v3.9.3 0 3749 560108.14 145624.41 3749 0 3749 410 562 410 0
SMTInterpol 0 3398 21257.74 13583.58 3398 0 3398 761 562 681 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 4143 830.11 1342.85 4143 0 4143 0 578 0 0
SMTInterpol 0 3333 10840.92 5312.10 3333 0 3333 113 1275 0 0
iProver v3.9.3 0 3106 28310.06 9863.13 3106 0 3106 0 1615 0 0