SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFDTLIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 774
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 715 43377.75 43470.76 715 0 715 59 0 59 0
iProver v3.9.3 0 501 51522.43 13802.63 542 0 542 232 0 232 0
SMTInterpol 0 164 8764.27 6542.25 165 0 165 609 0 437 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 715 43377.75 43470.76 715 0 715 59 0 59 0
iProver v3.9.3 0 542 194382.82 49913.31 542 0 542 232 0 232 0
SMTInterpol 0 165 10007.01 7501.18 165 0 165 609 0 437 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 715 43377.75 43470.76 715 0 715 59 0 59 0
iProver v3.9.3 0 542 194382.82 49913.31 542 0 542 232 0 232 0
SMTInterpol 0 165 10007.01 7501.18 165 0 165 609 0 437 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 661 2131.25 2212.51 661 0 661 0 113 0 0
iProver v3.9.3 0 321 5921.29 1820.51 321 0 321 0 453 0 0
SMTInterpol 0 150 884.85 333.46 150 0 150 0 624 0 0