SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

SMT-COMP 2025 Results - Parallel Track

Summary of all competition results for the Parallel Track.
Results are given ranked by performance for each scoring scheme (best solver is given as left-most solver).

QF_Bitvec

Scoring Scheme Winner Ranking
Sequential Performance -
Parallel Performance STP-Parti-Bitwuzla STP-Parti-Bitwuzla, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core
SAT Performance STP-Parti-Bitwuzla STP-Parti-Bitwuzla, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core
UNSAT Performance STP-Parti-Bitwuzla STP-Parti-Bitwuzla, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core
24 seconds Performance Bitwuzla Bitwuzla, STP-Parti-Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core

QF_Equality_Bitvec

Scoring Scheme Winner Ranking
Sequential Performance -
Parallel Performance Bitwuzla Bitwuzla, Yices2, Bitwuzla-32core, Bitwuzla-64core
SAT Performance Bitwuzla Bitwuzla, Yices2, Bitwuzla-32core, Bitwuzla-64core
UNSAT Performance Yices2 Yices2, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core
24 seconds Performance Bitwuzla Bitwuzla, Yices2, Bitwuzla-32core, Bitwuzla-64core

QF_Equality_LinearArith

Scoring Scheme Winner Ranking
Sequential Performance -
Parallel Performance SMTS SMTS, Yices2, SMTS (32 cores), SMTS (64 cores)
SAT Performance Yices2 Yices2, SMTS, SMTS (32 cores), SMTS (64 cores)
UNSAT Performance SMTS SMTS, Yices2, SMTS (32 cores), SMTS (64 cores)
24 seconds Performance Yices2 Yices2, SMTS (32 cores), SMTS (64 cores)

QF_LinearIntArith

Scoring Scheme Winner Ranking
Sequential Performance -
Parallel Performance SMTS SMTS, Z3-Parti-Z3pp, Yices2, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
SAT Performance SMTS SMTS, Z3-Parti-Z3pp, Yices2, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
UNSAT Performance Z3-Parti-Z3pp Z3-Parti-Z3pp, SMTS, Yices2, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
24 seconds Performance SMTS SMTS, Z3-Parti-Z3pp, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core

QF_LinearRealArith

Scoring Scheme Winner Ranking
Sequential Performance -
Parallel Performance SMTS SMTS, Yices2, Z3-Parti-Z3pp, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
SAT Performance SMTS SMTS, Yices2, Z3-Parti-Z3pp, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
UNSAT Performance SMTS SMTS, Yices2, Z3-Parti-Z3pp, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
24 seconds Performance SMTS SMTS, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core

QF_NonLinearIntArith

Scoring Scheme Winner Ranking
Sequential Performance -
Parallel Performance Z3-Parti-Z3pp Z3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
SAT Performance Z3-Parti-Z3pp Z3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
UNSAT Performance Z3-Parti-Z3pp Z3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
24 seconds Performance Z3-Parti-Z3pp Z3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core

QF_NonLinearRealArith

Scoring Scheme Winner Ranking
Sequential Performance -
Parallel Performance Z3-Parti-Z3pp Z3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
SAT Performance Z3-Parti-Z3pp Z3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
UNSAT Performance Yices2 Yices2, Z3-Parti-Z3pp, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
24 seconds Performance Yices2 Yices2, Z3-Parti-Z3pp, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core