SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UF (Model Validation Track)

Competition results for the QF_UF logic in the Model Validation Track. Chart

Results were generated on 2025-08-11

Benchmarks: 1571
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
OpenSMT OpenSMT OpenSMT - OpenSMT

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 1571 383.74 577.16 1571 1571 0 0 0 0
cvc5 0 1571 498.38 688.26 1571 1571 0 0 0 0
SMTInterpol 0 1571 3564.11 1596.37 1571 1571 0 0 0 0
Yices2 0 1570 278.69 472.78 1570 1570 1 0 0 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 1571 383.74 577.16 1571 1571 0 0 0 0
cvc5 0 1571 498.38 688.26 1571 1571 0 0 0 0
SMTInterpol 0 1571 3564.11 1596.37 1571 1571 0 0 0 0
Yices2 0 1570 278.69 472.78 1570 1570 1 0 0 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 1571 383.74 577.16 1571 1571 0 0 0 0
cvc5 0 1571 498.38 688.26 1571 1571 0 0 0 0
SMTInterpol 0 1571 3564.11 1596.37 1571 1571 0 0 0 0
Yices2 0 1570 278.69 472.78 1570 1570 1 0 0 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 1571 383.74 577.16 1571 1571 0 0 0 0
cvc5 0 1571 498.38 688.26 1571 1571 0 0 0 0
SMTInterpol 0 1571 3564.11 1596.37 1571 1571 0 0 0 0
Yices2 0 1570 278.69 472.78 1570 1570 1 0 0 0