SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFDTNIRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 2043
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 1870 1679.43 1909.86 1870 0 1870 173 0 79 0
iProver v3.9.3 0 1454 60355.98 16415.39 1581 0 1581 462 0 462 0
SMTInterpol 0 1354 10850.87 6972.93 1354 0 1354 689 0 419 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 1870 1679.43 1909.86 1870 0 1870 173 0 79 0
iProver v3.9.3 0 1581 436299.69 111111.77 1581 0 1581 462 0 462 0
SMTInterpol 0 1354 10850.87 6972.93 1354 0 1354 689 0 419 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 1870 1679.43 1909.86 1870 0 1870 4 169 4 0
iProver v3.9.3 0 1581 436299.69 111111.77 1581 0 1581 293 169 293 0
SMTInterpol 0 1354 10850.87 6972.93 1354 0 1354 520 169 278 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 1866 394.41 624.08 1866 0 1866 94 83 0 0
SMTInterpol 0 1327 4611.54 2007.69 1327 0 1327 86 630 0 0
iProver v3.9.3 0 1304 10738.21 3620.85 1304 0 1304 0 739 0 0