SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LRA (Model Validation Track)

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

Results were generated on 2025-08-11

Benchmarks: 497
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 - OpenSMT

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 483 12202.81 12264.44 483 483 14 0 14 0
Yices2 0 482 11352.44 11413.04 482 482 15 0 15 0
SMTInterpol 0 445 26853.58 23713.99 445 445 52 0 52 0
cvc5 0 366 2309.06 2353.44 366 366 131 0 131 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 483 12202.81 12264.44 483 483 14 0 14 0
Yices2 0 482 11352.44 11413.04 482 482 15 0 15 0
SMTInterpol 0 445 26853.58 23713.99 445 445 52 0 52 0
cvc5 0 366 2309.06 2353.44 366 366 131 0 131 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 483 12202.81 12264.44 483 483 14 0 14 0
Yices2 0 482 11352.44 11413.04 482 482 15 0 15 0
SMTInterpol 0 445 26853.58 23713.99 445 445 52 0 52 0
cvc5 0 366 2309.06 2353.44 366 366 131 0 131 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 433 932.36 985.89 433 433 0 64 0 0
Yices2 0 431 587.37 640.34 431 431 0 66 0 0
SMTInterpol 0 355 1973.33 914.71 355 355 0 142 0 0
cvc5 0 351 404.10 446.47 351 351 0 146 0 0