SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFLIA (Model Validation Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 299 1872.61 1355.89 299 299 1 0 1 0
cvc5 0 298 1283.49 1320.19 298 298 2 0 2 0
Yices2 0 297 791.89 828.96 297 297 3 0 3 0
OpenSMT 0 296 1565.76 1602.85 296 296 4 0 4 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 299 1872.61 1355.89 299 299 1 0 1 0
cvc5 0 298 1283.49 1320.19 298 298 2 0 2 0
Yices2 0 297 791.89 828.96 297 297 3 0 3 0
OpenSMT 0 296 1565.76 1602.85 296 296 4 0 4 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 299 1872.61 1355.89 299 299 1 0 1 0
cvc5 0 298 1283.49 1320.19 298 298 2 0 2 0
Yices2 0 297 791.89 828.96 297 297 3 0 3 0
OpenSMT 0 296 1565.76 1602.85 296 296 4 0 4 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 294 110.64 147.24 294 294 0 6 0 0
cvc5 0 293 214.50 250.43 293 293 0 7 0 0
SMTInterpol 0 293 745.99 352.60 293 293 0 7 0 0
OpenSMT 0 290 427.60 463.66 290 290 0 10 0 0