SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_LinearArith (Parallel Track)

Competition results for the QF_Equality_LinearArith division in the Parallel Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
- SMTS Yices2 SMTS Yices2

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTS 0 15 549824.76 4812.85 15 2 13 53 0 46 0
Yices2 0 10 443774.95 3480.68 10 7 3 58 0 58 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 68 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 68 0 0 0
n: non-competing solver

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 7 355486.10 2787.29 7 7 0 6 55 6 0
SMTS 0 2 30476.05 241.20 2 2 0 11 55 10 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 13 55 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 13 55 0 0
n: non-competing solver

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTS 0 13 519348.70 4571.65 13 0 13 23 32 21 0
Yices2 0 3 88288.86 693.39 3 0 3 33 32 33 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 36 32 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 36 32 0 0
n: non-competing solver

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 1 2772.26 22.77 1 1 0 0 67 0 0
SMTS (32 cores) n 0 0 0.00 0.00 0 0 0 68 0 0 0
SMTS (64 cores) n 0 0 0.00 0.00 0 0 0 68 0 0 0
n: non-competing solver