SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFDTNIRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 725
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 573 663.59 734.25 573 0 573 152 0 89 0
iProver v3.9.3 0 482 38978.39 10275.94 502 0 502 223 0 223 0
SMTInterpol 0 451 1453.03 719.78 451 0 451 274 0 273 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 573 663.59 734.25 573 0 573 152 0 89 0
iProver v3.9.3 0 502 97806.28 25068.38 502 0 502 223 0 223 0
SMTInterpol 0 451 1453.03 719.78 451 0 451 274 0 273 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 573 663.59 734.25 573 0 573 1 151 0 0
iProver v3.9.3 0 502 97806.28 25068.38 502 0 502 72 151 72 0
SMTInterpol 0 451 1453.03 719.78 451 0 451 123 151 122 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 572 119.27 189.75 572 0 572 63 90 0 0
SMTInterpol 0 451 1453.03 719.78 451 0 451 1 273 0 0
iProver v3.9.3 0 398 5328.48 1662.85 398 0 398 0 327 0 0