SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFDTNIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 504
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 366 55708.03 55761.13 366 0 366 138 0 132 0
iProver v3.9.3 0 168 31413.53 8204.61 219 0 219 285 0 246 39
SMTInterpol 0 54 1475.01 616.07 54 0 54 450 0 195 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 366 55708.03 55761.13 366 0 366 138 0 132 0
iProver v3.9.3 0 219 168468.77 42850.28 219 0 219 285 0 246 39
SMTInterpol 0 54 1475.01 616.07 54 0 54 450 0 195 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 366 55708.03 55761.13 366 0 366 138 0 132 0
iProver v3.9.3 0 219 168468.77 42850.28 219 0 219 285 0 246 39
SMTInterpol 0 54 1475.01 616.07 54 0 54 450 0 195 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 199 831.08 855.65 199 0 199 1 304 0 0
iProver v3.9.3 0 79 857.02 275.61 79 0 79 0 425 0 0
SMTInterpol 0 47 702.31 297.06 47 0 47 0 457 0 0