SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_IDL (Model Validation Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 663 18100.18 18183.75 663 663 73 0 72 0
OpenSMT 0 608 40013.70 40094.30 608 608 128 0 128 0
cvc5 0 594 49413.12 49493.03 594 594 142 0 138 4
SMTInterpol 0 380 26144.56 22160.38 380 380 356 0 208 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 663 18100.18 18183.75 663 663 73 0 72 0
OpenSMT 0 608 40013.70 40094.30 608 608 128 0 128 0
cvc5 0 594 49413.12 49493.03 594 594 142 0 138 4
SMTInterpol 0 380 26144.56 22160.38 380 380 356 0 208 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 663 18100.18 18183.75 663 663 73 0 72 0
OpenSMT 0 608 40013.70 40094.30 608 608 128 0 128 0
cvc5 0 594 49413.12 49493.03 594 594 142 0 138 4
SMTInterpol 0 380 26144.56 22160.38 380 380 356 0 208 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 599 936.64 1009.93 599 599 1 136 0 0
OpenSMT 0 411 1373.16 1423.91 411 411 0 325 0 0
cvc5 0 388 1253.53 1301.08 388 388 0 348 0 0
SMTInterpol 0 272 2750.85 1300.92 272 272 120 344 0 0