SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LinearRealArith (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

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 591 11946.41 12020.45 591 591 15 0 15 0
OpenSMT 0 590 20671.54 20747.41 590 590 16 0 16 0
SMTInterpol 0 548 31291.92 27288.02 548 548 58 0 58 0
cvc5 0 471 3437.17 3494.40 471 471 135 0 135 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 591 11946.41 12020.45 591 591 15 0 15 0
OpenSMT 0 590 20671.54 20747.41 590 590 16 0 16 0
SMTInterpol 0 548 31291.92 27288.02 548 548 58 0 58 0
cvc5 0 471 3437.17 3494.40 471 471 135 0 135 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 591 11946.41 12020.45 591 591 15 0 15 0
OpenSMT 0 590 20671.54 20747.41 590 590 16 0 16 0
SMTInterpol 0 548 31291.92 27288.02 548 548 58 0 58 0
cvc5 0 471 3437.17 3494.40 471 471 135 0 135 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 534 675.90 741.46 534 534 0 72 0 0
OpenSMT 0 518 1121.96 1185.93 518 518 0 88 0 0
cvc5 0 448 752.69 806.81 448 448 0 158 0 0
SMTInterpol 0 435 2781.07 1298.27 435 435 0 171 0 0