SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_LinearArith (Model Validation Track)

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

Results were generated on 2025-08-11

Benchmarks: 891
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 - SMTInterpol

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 875 10359.08 10469.75 875 875 16 0 16 0
SMTInterpol 0 863 14112.21 10956.23 863 863 28 0 28 0
cvc5 0 857 26524.00 26633.68 857 857 34 0 34 0
Yices2 0 823 15704.73 15809.28 823 823 68 0 68 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 875 10359.08 10469.75 875 875 16 0 16 0
SMTInterpol 0 863 14112.21 10956.23 863 863 28 0 28 0
cvc5 0 857 26524.00 26633.68 857 857 34 0 34 0
Yices2 0 823 15704.73 15809.28 823 823 68 0 68 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 875 10359.08 10469.75 875 875 16 0 16 0
SMTInterpol 0 863 14112.21 10956.23 863 863 28 0 28 0
cvc5 0 857 26524.00 26633.68 857 857 34 0 34 0
Yices2 0 823 15704.73 15809.28 823 823 68 0 68 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 835 3380.24 1472.30 835 835 0 56 0 0
OpenSMT 0 824 1228.24 1331.02 824 824 0 67 0 0
Yices2 0 785 261.28 358.75 785 785 0 106 0 0
cvc5 0 778 454.33 550.04 778 778 0 113 0 0