SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_LinearRealArith (Parallel Track)

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

Results were generated on 2026-07-25

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
-z3-parallelOpenSMT-SMTSz3-parallelOpenSMT-SMTS

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT-SMTS ne022
(base +4)		972034.917733.23221111460460
z3-parallel04393705.213343.55404640640
OpenSMT-SMTS-base n0187200.967204.6618711500500
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT-SMTS011
(base +4)		715199.655681.721111055250
z3-parallel000.000.000001652160
OpenSMT-SMTS-base n073619.413621.1577095290
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT-SMTS ne011
(base +0)		256835.262051.501101184980
z3-parallel04393705.213343.554041549150
OpenSMT-SMTS-base n0113581.563583.511101184980
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT-SMTS012515.0720.9911006700
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver