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 SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceSTP-Parti-BitwuzlaSTP-Parti-Bitwuzla, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core
SAT PerformanceSTP-Parti-BitwuzlaSTP-Parti-Bitwuzla, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core
UNSAT PerformanceSTP-Parti-BitwuzlaSTP-Parti-Bitwuzla, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core
24 seconds PerformanceBitwuzlaBitwuzla, STP-Parti-Bitwuzla, Bitwuzla-32core, Bitwuzla-64core, STP-Parti-Bitwuzla-16core, STP-Parti-Bitwuzla-32core, STP-Parti-Bitwuzla-64core

QF_Equality_Bitvec

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceBitwuzlaBitwuzla, Yices2, Bitwuzla-32core, Bitwuzla-64core
SAT PerformanceBitwuzlaBitwuzla, Yices2, Bitwuzla-32core, Bitwuzla-64core
UNSAT PerformanceYices2Yices2, Bitwuzla, Bitwuzla-32core, Bitwuzla-64core
24 seconds PerformanceBitwuzlaBitwuzla, Yices2, Bitwuzla-32core, Bitwuzla-64core

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceSMTSSMTS, Yices2, SMTS (32 cores), SMTS (64 cores)
SAT PerformanceYices2Yices2, SMTS, SMTS (32 cores), SMTS (64 cores)
UNSAT PerformanceSMTSSMTS, Yices2, SMTS (32 cores), SMTS (64 cores)
24 seconds PerformanceYices2Yices2, SMTS (32 cores), SMTS (64 cores)

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceSMTSSMTS, Z3-Parti-Z3pp, Yices2, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
SAT PerformanceSMTSSMTS, Z3-Parti-Z3pp, Yices2, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
UNSAT PerformanceZ3-Parti-Z3ppZ3-Parti-Z3pp, SMTS, Yices2, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
24 seconds PerformanceSMTSSMTS, Z3-Parti-Z3pp, SMTS (32 cores), SMTS (64 cores), Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core

QF_LinearRealArith

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

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceZ3-Parti-Z3ppZ3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
SAT PerformanceZ3-Parti-Z3ppZ3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
UNSAT PerformanceZ3-Parti-Z3ppZ3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
24 seconds PerformanceZ3-Parti-Z3ppZ3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core

QF_NonLinearRealArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceZ3-Parti-Z3ppZ3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
SAT PerformanceZ3-Parti-Z3ppZ3-Parti-Z3pp, Yices2, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
UNSAT PerformanceYices2Yices2, Z3-Parti-Z3pp, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core
24 seconds PerformanceYices2Yices2, Z3-Parti-Z3pp, Z3-Parti-Z3pp-16core, Z3-Parti-Z3pp-32core, Z3-Parti-Z3pp-64core