SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

SMT-COMP 2025 Results - Single Query Track

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

Arith

Scoring SchemeWinnerRanking
Sequential PerformanceZ3-alphaZ3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, iProver v3.9.3, SMTInterpol, SMT-RAT, Amaya, Z3-alpha-base
Parallel PerformanceZ3-alphaZ3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, iProver v3.9.3, SMTInterpol, SMT-RAT, Amaya, Z3-alpha-base
SAT PerformanceZ3-alphaZ3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, SMTInterpol, SMT-RAT, iProver v3.9.3, Amaya, Z3-alpha-base
UNSAT PerformanceZ3-alphaZ3-alpha, cvc5, YicesQS, UltimateEliminator+MathSAT, iProver v3.9.3, Amaya, SMTInterpol, SMT-RAT, Z3-alpha-base
24 seconds PerformanceZ3-alphaZ3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, iProver v3.9.3, SMTInterpol, SMT-RAT, Amaya, Z3-alpha-base

Bitvec

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, YicesQS, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
Parallel Performancecvc5cvc5, YicesQS, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
SAT PerformanceBitwuzlaBitwuzla, YicesQS, cvc5, UltimateEliminator+MathSAT, SMTInterpol
UNSAT Performancecvc5cvc5, YicesQS, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
24 seconds PerformanceYicesQSYicesQS, Bitwuzla, cvc5, UltimateEliminator+MathSAT, SMTInterpol

Equality

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performancecvc5cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT
SAT Performancecvc5cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT
UNSAT Performancecvc5cvc5, iProver v3.9.3, SMTInterpol, Yices2, UltimateEliminator+MathSAT
24 seconds Performancecvc5cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT

Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol
Parallel Performancecvc5cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol
SAT Performancecvc5cvc5, SMTInterpol, UltimateEliminator+MathSAT, iProver v3.9.3
UNSAT Performancecvc5cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol
24 seconds Performancecvc5cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol

Equality_MachineArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT
Parallel Performancecvc5cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT
SAT Performancecvc5cvc5, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
UNSAT Performancecvc5cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT
24 seconds Performancecvc5cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT

Equality_NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performancecvc5cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT
SAT Performancecvc5cvc5, UltimateEliminator+MathSAT, SMTInterpol, iProver v3.9.3
UNSAT Performancecvc5cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT
24 seconds Performancecvc5cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT

FPArith

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, cvc5, UltimateEliminator+MathSAT
Parallel PerformanceBitwuzlaBitwuzla, cvc5, UltimateEliminator+MathSAT
SAT PerformanceBitwuzlaBitwuzla, cvc5, UltimateEliminator+MathSAT
UNSAT PerformanceBitwuzlaBitwuzla, cvc5, UltimateEliminator+MathSAT
24 seconds PerformanceBitwuzlaBitwuzla, cvc5, UltimateEliminator+MathSAT

QF_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzla-MachBVBitwuzla-MachBV, Bitwuzla, Yices2, cvc5, z3siri, Z3-alpha, bv_decide-nokernel, Z3-Owl, bv_decide, SMTInterpol, Bitwuzla-MachBV-base, Z3-alpha-base, z3siri-base, Z3-Owl-base
Parallel PerformanceBitwuzla-MachBVBitwuzla-MachBV, Bitwuzla, Yices2, cvc5, Z3-alpha, z3siri, bv_decide-nokernel, Z3-Owl, bv_decide, SMTInterpol, Bitwuzla-MachBV-base, Z3-alpha-base, z3siri-base, Z3-Owl-base
SAT PerformanceBitwuzlaBitwuzla, Bitwuzla-MachBV, Yices2, cvc5, bv_decide-nokernel, bv_decide, Z3-alpha, Z3-Owl, z3siri, SMTInterpol, Bitwuzla-MachBV-base, Z3-alpha-base, z3siri-base, Z3-Owl-base
UNSAT PerformanceBitwuzla-MachBVBitwuzla-MachBV, Bitwuzla, Yices2, cvc5, z3siri, Z3-alpha, Z3-Owl, bv_decide-nokernel, bv_decide, SMTInterpol, Bitwuzla-MachBV-base, Z3-alpha-base, z3siri-base, Z3-Owl-base
24 seconds PerformanceBitwuzla-MachBVBitwuzla-MachBV, Bitwuzla, Yices2, cvc5, Z3-alpha, z3siri, Z3-Owl, bv_decide-nokernel, bv_decide, SMTInterpol, Bitwuzla-MachBV-base, Z3-alpha-base, z3siri-base, Z3-Owl-base

QF_Datatypes

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, SMTInterpol
Parallel Performancecvc5cvc5, SMTInterpol
SAT Performancecvc5cvc5, SMTInterpol
UNSAT Performancecvc5cvc5, SMTInterpol
24 seconds PerformanceSMTInterpolSMTInterpol, cvc5

QF_Equality

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, OpenSMT, cvc5, SMTInterpol
Parallel PerformanceYices2Yices2, OpenSMT, cvc5, SMTInterpol
SAT PerformanceYices2Yices2, OpenSMT, cvc5, SMTInterpol
UNSAT PerformanceYices2Yices2, OpenSMT, cvc5, SMTInterpol
24 seconds PerformanceYices2Yices2, OpenSMT, cvc5, SMTInterpol

QF_Equality_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base
Parallel PerformanceBitwuzlaBitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base
SAT PerformanceBitwuzlaBitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base
UNSAT PerformanceBitwuzlaBitwuzla, Yices2, cvc5, Z3-Owl, SMTInterpol, Z3-Owl-base
24 seconds PerformanceBitwuzlaBitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpolSMTInterpol, cvc5, OpenSMT, Yices2
Parallel PerformanceSMTInterpolSMTInterpol, cvc5, OpenSMT, Yices2
SAT PerformanceSMTInterpolSMTInterpol, cvc5, OpenSMT, Yices2
UNSAT PerformanceOpenSMTOpenSMT, cvc5, Yices2, SMTInterpol
24 seconds PerformanceSMTInterpolSMTInterpol, Yices2, cvc5, OpenSMT

QF_Equality_NonLinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, cvc5, SMTInterpol
Parallel PerformanceYices2Yices2, cvc5, SMTInterpol
SAT PerformanceYices2Yices2, cvc5, SMTInterpol
UNSAT Performancecvc5cvc5, Yices2, SMTInterpol
24 seconds PerformanceYices2Yices2, cvc5, SMTInterpol

QF_FPArith

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base
Parallel PerformanceBitwuzlaBitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base
SAT PerformanceBitwuzlaBitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base
UNSAT PerformanceBitwuzlaBitwuzla, cvc5, COLIBRI, colibri2, Z3-Owl, Z3-Owl-base
24 seconds PerformanceBitwuzlaBitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceOpenSMTOpenSMT, Yices2, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
Parallel PerformanceOpenSMTOpenSMT, Yices2, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
SAT PerformanceZ3-alphaZ3-alpha, OpenSMT, cvc5, Yices2, SMTInterpol, Z3-alpha-base
UNSAT PerformanceOpenSMTOpenSMT, Yices2, cvc5, SMTInterpol, Z3-alpha, Z3-alpha-base
24 seconds PerformanceYices2Yices2, Z3-alpha, OpenSMT, cvc5, SMTInterpol, Z3-alpha-base

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, OpenSMT, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
Parallel PerformanceYices2Yices2, OpenSMT, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
SAT PerformanceOpenSMTOpenSMT, Yices2, Z3-alpha, cvc5, SMTInterpol, Z3-alpha-base
UNSAT PerformanceYices2Yices2, cvc5, OpenSMT, Z3-alpha, SMTInterpol, Z3-alpha-base
24 seconds PerformanceYices2Yices2, OpenSMT, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceZ3-alphaZ3-alpha, z3siri, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
Parallel PerformanceZ3-alphaZ3-alpha, z3siri, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
SAT PerformanceZ3-alphaZ3-alpha, z3siri, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
UNSAT Performancez3siriz3siri, Z3-alpha, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
24 seconds PerformanceZ3-alphaZ3-alpha, Yices2, z3siri, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base

QF_NonLinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceZ3-alphaZ3-alpha, z3siri, cvc5, Yices2, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
Parallel PerformanceZ3-alphaZ3-alpha, z3siri, cvc5, Yices2, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
SAT PerformanceZ3-alphaZ3-alpha, z3siri, Yices2, cvc5, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
UNSAT PerformanceZ3-alphaZ3-alpha, cvc5, z3siri, Yices2, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
24 seconds PerformanceZ3-alphaZ3-alpha, Yices2, cvc5, SMT-RAT, z3siri, SMTInterpol, z3siri-base, Z3-alpha-base

QF_Strings

Scoring SchemeWinnerRanking
Sequential PerformanceZ3-Noodler-MochaZ3-Noodler-Mocha, Z3-Noodler, OSTRICH, cvc5, Z3-alpha, Z3-Noodler-Mocha-base, Z3-alpha-base, Z3-Noodler-base
Parallel PerformanceZ3-Noodler-MochaZ3-Noodler-Mocha, Z3-Noodler, OSTRICH, cvc5, Z3-alpha, Z3-Noodler-Mocha-base, Z3-alpha-base, Z3-Noodler-base
SAT PerformanceZ3-Noodler-MochaZ3-Noodler-Mocha, Z3-Noodler, OSTRICH, cvc5, Z3-alpha, Z3-Noodler-Mocha-base, Z3-alpha-base, Z3-Noodler-base
UNSAT PerformanceZ3-Noodler-MochaZ3-Noodler-Mocha, Z3-Noodler, OSTRICH, Z3-alpha, cvc5, Z3-Noodler-Mocha-base, Z3-Noodler-base, Z3-alpha-base
24 seconds PerformanceZ3-Noodler-MochaZ3-Noodler-Mocha, Z3-Noodler, Z3-alpha, cvc5, OSTRICH, Z3-Noodler-Mocha-base, Z3-Noodler-base, Z3-alpha-base