SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LIA (Model Validation Track)

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

Results were generated on 2025-08-11

Benchmarks: 4158
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 - Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 3975 197961.09 198484.77 3975 3975 183 0 183 0
Yices2 0 3870 44188.31 44669.80 3870 3870 288 0 288 0
SMTInterpol 0 3715 118582.31 97797.95 3717 3717 441 0 437 0
cvc5 0 3220 121367.70 121779.75 3220 3220 938 0 938 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 3975 197961.09 198484.77 3975 3975 183 0 183 0
Yices2 0 3870 44188.31 44669.80 3870 3870 288 0 288 0
SMTInterpol 0 3717 121099.59 99881.17 3717 3717 441 0 437 0
cvc5 0 3220 121367.70 121779.75 3220 3220 938 0 938 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 3975 197961.09 198484.77 3975 3975 183 0 183 0
Yices2 0 3870 44188.31 44669.80 3870 3870 288 0 288 0
SMTInterpol 0 3717 121099.59 99881.17 3717 3717 441 0 437 0
cvc5 0 3220 121367.70 121779.75 3220 3220 938 0 938 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 3708 2488.02 2944.32 3708 3708 0 450 0 0
OpenSMT 0 3210 4131.54 4527.03 3210 3210 0 948 0 0
SMTInterpol 0 3126 12618.86 6188.19 3126 3126 0 1032 0 0
cvc5 0 2931 2633.73 2990.75 2931 2931 0 1227 0 0