SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFLRA (Model Validation Track)

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

Results were generated on 2025-08-11

Benchmarks: 385
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 383 295.34 342.81 383 383 2 0 2 0
SMTInterpol 0 383 3147.32 1882.55 383 383 2 0 2 0
cvc5 0 382 337.98 385.12 382 382 3 0 3 0
OpenSMT 0 378 920.18 967.46 378 378 7 0 7 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 383 295.34 342.81 383 383 2 0 2 0
SMTInterpol 0 383 3147.32 1882.55 383 383 2 0 2 0
cvc5 0 382 337.98 385.12 382 382 3 0 3 0
OpenSMT 0 378 920.18 967.46 378 378 7 0 7 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 383 295.34 342.81 383 383 2 0 2 0
SMTInterpol 0 383 3147.32 1882.55 383 383 2 0 2 0
cvc5 0 382 337.98 385.12 382 382 3 0 3 0
OpenSMT 0 378 920.18 967.46 378 378 7 0 7 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 382 85.76 133.08 382 382 0 3 0 0
cvc5 0 378 164.29 210.90 378 378 0 7 0 0
SMTInterpol 0 378 1204.18 514.38 378 378 0 7 0 0
OpenSMT 0 372 296.47 342.89 372 372 0 13 0 0