SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ADT_LinArith (Model Validation Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 771 4426.70 3421.82 771 771 1 0 0 0
cvc5 0 760 6741.44 6834.41 760 760 12 0 12 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 771 4426.70 3421.82 771 771 1 0 0 0
cvc5 0 760 6741.44 6834.41 760 760 12 0 12 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 771 4426.70 3421.82 771 771 1 0 0 0
cvc5 0 760 6741.44 6834.41 760 760 12 0 12 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 757 1392.67 707.43 757 757 1 14 0 0
cvc5 0 730 654.22 742.39 730 730 0 42 0 0