SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LinearIntArith (Model Validation Track)

Competition results for the QF_LinearIntArith division in the Model Validation Track. Chart

Results were generated on 2025-08-11

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

Logics:

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 4583 237974.80 238579.07 4583 4583 311 1 311 0
Yices2 0 4534 62288.73 62853.91 4534 4534 361 0 360 0
SMTInterpol 0 4096 144744.98 119966.73 4098 4098 797 0 645 0
cvc5 0 3815 170783.41 171275.49 3815 3815 1080 0 1076 4

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 4583 237974.80 238579.07 4583 4583 311 1 311 0
Yices2 0 4534 62288.73 62853.91 4534 4534 361 0 360 0
SMTInterpol 0 4098 147262.26 122049.94 4098 4098 797 0 645 0
cvc5 0 3815 170783.41 171275.49 3815 3815 1080 0 1076 4

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 4583 237974.80 238579.07 4583 4583 311 1 311 0
Yices2 0 4534 62288.73 62853.91 4534 4534 361 0 360 0
SMTInterpol 0 4098 147262.26 122049.94 4098 4098 797 0 645 0
cvc5 0 3815 170783.41 171275.49 3815 3815 1080 0 1076 4

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 4308 3424.89 3954.61 4308 4308 1 586 0 0
OpenSMT 0 3621 5504.70 5950.94 3621 3621 0 1274 0 0
SMTInterpol 0 3399 15387.82 7497.51 3399 3399 120 1376 0 0
cvc5 0 3320 3889.86 4294.54 3320 3320 0 1575 0 0