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 Scheme Winner Ranking
Sequential Performance Z3-alpha Z3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, iProver v3.9.3, SMTInterpol, SMT-RAT, Amaya, Z3-alpha-base
Parallel Performance Z3-alpha Z3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, iProver v3.9.3, SMTInterpol, SMT-RAT, Amaya, Z3-alpha-base
SAT Performance Z3-alpha Z3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, SMTInterpol, SMT-RAT, iProver v3.9.3, Amaya, Z3-alpha-base
UNSAT Performance Z3-alpha Z3-alpha, cvc5, YicesQS, UltimateEliminator+MathSAT, iProver v3.9.3, Amaya, SMTInterpol, SMT-RAT, Z3-alpha-base
24 seconds Performance Z3-alpha Z3-alpha, YicesQS, cvc5, UltimateEliminator+MathSAT, iProver v3.9.3, SMTInterpol, SMT-RAT, Amaya, Z3-alpha-base

Bitvec

Scoring Scheme Winner Ranking
Sequential Performance cvc5 cvc5, YicesQS, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
Parallel Performance cvc5 cvc5, YicesQS, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
SAT Performance Bitwuzla Bitwuzla, YicesQS, cvc5, UltimateEliminator+MathSAT, SMTInterpol
UNSAT Performance cvc5 cvc5, YicesQS, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
24 seconds Performance YicesQS YicesQS, Bitwuzla, cvc5, UltimateEliminator+MathSAT, SMTInterpol

Equality

Scoring Scheme Winner Ranking
Sequential Performance cvc5 cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performance cvc5 cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT
SAT Performance cvc5 cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT
UNSAT Performance cvc5 cvc5, iProver v3.9.3, SMTInterpol, Yices2, UltimateEliminator+MathSAT
24 seconds Performance cvc5 cvc5, iProver v3.9.3, Yices2, SMTInterpol, UltimateEliminator+MathSAT

Equality_LinearArith

Scoring Scheme Winner Ranking
Sequential Performance cvc5 cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol
Parallel Performance cvc5 cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol
SAT Performance cvc5 cvc5, SMTInterpol, UltimateEliminator+MathSAT, iProver v3.9.3
UNSAT Performance cvc5 cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol
24 seconds Performance cvc5 cvc5, iProver v3.9.3, UltimateEliminator+MathSAT, SMTInterpol

Equality_MachineArith

Scoring Scheme Winner Ranking
Sequential Performance cvc5 cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT
Parallel Performance cvc5 cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT
SAT Performance cvc5 cvc5, Bitwuzla, UltimateEliminator+MathSAT, SMTInterpol
UNSAT Performance cvc5 cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT
24 seconds Performance cvc5 cvc5, SMTInterpol, Bitwuzla, UltimateEliminator+MathSAT

Equality_NonLinearArith

Scoring Scheme Winner Ranking
Sequential Performance cvc5 cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performance cvc5 cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT
SAT Performance cvc5 cvc5, UltimateEliminator+MathSAT, SMTInterpol, iProver v3.9.3
UNSAT Performance cvc5 cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT
24 seconds Performance cvc5 cvc5, iProver v3.9.3, SMTInterpol, UltimateEliminator+MathSAT

FPArith

Scoring Scheme Winner Ranking
Sequential Performance Bitwuzla Bitwuzla, cvc5, UltimateEliminator+MathSAT
Parallel Performance Bitwuzla Bitwuzla, cvc5, UltimateEliminator+MathSAT
SAT Performance Bitwuzla Bitwuzla, cvc5, UltimateEliminator+MathSAT
UNSAT Performance Bitwuzla Bitwuzla, cvc5, UltimateEliminator+MathSAT
24 seconds Performance Bitwuzla Bitwuzla, cvc5, UltimateEliminator+MathSAT

QF_Bitvec

Scoring Scheme Winner Ranking
Sequential Performance Bitwuzla-MachBV Bitwuzla-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 Performance Bitwuzla-MachBV Bitwuzla-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 Performance Bitwuzla Bitwuzla, 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 Performance Bitwuzla-MachBV Bitwuzla-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 Performance Bitwuzla-MachBV Bitwuzla-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 Scheme Winner Ranking
Sequential Performance cvc5 cvc5, SMTInterpol
Parallel Performance cvc5 cvc5, SMTInterpol
SAT Performance cvc5 cvc5, SMTInterpol
UNSAT Performance cvc5 cvc5, SMTInterpol
24 seconds Performance SMTInterpol SMTInterpol, cvc5

QF_Equality

Scoring Scheme Winner Ranking
Sequential Performance Yices2 Yices2, OpenSMT, cvc5, SMTInterpol
Parallel Performance Yices2 Yices2, OpenSMT, cvc5, SMTInterpol
SAT Performance Yices2 Yices2, OpenSMT, cvc5, SMTInterpol
UNSAT Performance Yices2 Yices2, OpenSMT, cvc5, SMTInterpol
24 seconds Performance Yices2 Yices2, OpenSMT, cvc5, SMTInterpol

QF_Equality_Bitvec

Scoring Scheme Winner Ranking
Sequential Performance Bitwuzla Bitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base
Parallel Performance Bitwuzla Bitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base
SAT Performance Bitwuzla Bitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base
UNSAT Performance Bitwuzla Bitwuzla, Yices2, cvc5, Z3-Owl, SMTInterpol, Z3-Owl-base
24 seconds Performance Bitwuzla Bitwuzla, Yices2, Z3-Owl, cvc5, SMTInterpol, Z3-Owl-base

QF_Equality_LinearArith

Scoring Scheme Winner Ranking
Sequential Performance SMTInterpol SMTInterpol, cvc5, OpenSMT, Yices2
Parallel Performance SMTInterpol SMTInterpol, cvc5, OpenSMT, Yices2
SAT Performance SMTInterpol SMTInterpol, cvc5, OpenSMT, Yices2
UNSAT Performance OpenSMT OpenSMT, cvc5, Yices2, SMTInterpol
24 seconds Performance SMTInterpol SMTInterpol, Yices2, cvc5, OpenSMT

QF_Equality_NonLinearArith

Scoring Scheme Winner Ranking
Sequential Performance Yices2 Yices2, cvc5, SMTInterpol
Parallel Performance Yices2 Yices2, cvc5, SMTInterpol
SAT Performance Yices2 Yices2, cvc5, SMTInterpol
UNSAT Performance cvc5 cvc5, Yices2, SMTInterpol
24 seconds Performance Yices2 Yices2, cvc5, SMTInterpol

QF_FPArith

Scoring Scheme Winner Ranking
Sequential Performance Bitwuzla Bitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base
Parallel Performance Bitwuzla Bitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base
SAT Performance Bitwuzla Bitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base
UNSAT Performance Bitwuzla Bitwuzla, cvc5, COLIBRI, colibri2, Z3-Owl, Z3-Owl-base
24 seconds Performance Bitwuzla Bitwuzla, cvc5, colibri2, Z3-Owl, COLIBRI, Z3-Owl-base

QF_LinearIntArith

Scoring Scheme Winner Ranking
Sequential Performance OpenSMT OpenSMT, Yices2, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
Parallel Performance OpenSMT OpenSMT, Yices2, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
SAT Performance Z3-alpha Z3-alpha, OpenSMT, cvc5, Yices2, SMTInterpol, Z3-alpha-base
UNSAT Performance OpenSMT OpenSMT, Yices2, cvc5, SMTInterpol, Z3-alpha, Z3-alpha-base
24 seconds Performance Yices2 Yices2, Z3-alpha, OpenSMT, cvc5, SMTInterpol, Z3-alpha-base

QF_LinearRealArith

Scoring Scheme Winner Ranking
Sequential Performance Yices2 Yices2, OpenSMT, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
Parallel Performance Yices2 Yices2, OpenSMT, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base
SAT Performance OpenSMT OpenSMT, Yices2, Z3-alpha, cvc5, SMTInterpol, Z3-alpha-base
UNSAT Performance Yices2 Yices2, cvc5, OpenSMT, Z3-alpha, SMTInterpol, Z3-alpha-base
24 seconds Performance Yices2 Yices2, OpenSMT, cvc5, Z3-alpha, SMTInterpol, Z3-alpha-base

QF_NonLinearIntArith

Scoring Scheme Winner Ranking
Sequential Performance Z3-alpha Z3-alpha, z3siri, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
Parallel Performance Z3-alpha Z3-alpha, z3siri, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
SAT Performance Z3-alpha Z3-alpha, z3siri, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
UNSAT Performance z3siri z3siri, Z3-alpha, Yices2, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base
24 seconds Performance Z3-alpha Z3-alpha, Yices2, z3siri, cvc5, SMTInterpol, Z3-alpha-base, z3siri-base

QF_NonLinearRealArith

Scoring Scheme Winner Ranking
Sequential Performance Z3-alpha Z3-alpha, z3siri, cvc5, Yices2, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
Parallel Performance Z3-alpha Z3-alpha, z3siri, cvc5, Yices2, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
SAT Performance Z3-alpha Z3-alpha, z3siri, Yices2, cvc5, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
UNSAT Performance Z3-alpha Z3-alpha, cvc5, z3siri, Yices2, SMT-RAT, SMTInterpol, Z3-alpha-base, z3siri-base
24 seconds Performance Z3-alpha Z3-alpha, Yices2, cvc5, SMT-RAT, z3siri, SMTInterpol, z3siri-base, Z3-alpha-base

QF_Strings

Scoring Scheme Winner Ranking
Sequential Performance Z3-Noodler-Mocha Z3-Noodler-Mocha, Z3-Noodler, OSTRICH, cvc5, Z3-alpha, Z3-Noodler-Mocha-base, Z3-alpha-base, Z3-Noodler-base
Parallel Performance Z3-Noodler-Mocha Z3-Noodler-Mocha, Z3-Noodler, OSTRICH, cvc5, Z3-alpha, Z3-Noodler-Mocha-base, Z3-alpha-base, Z3-Noodler-base
SAT Performance Z3-Noodler-Mocha Z3-Noodler-Mocha, Z3-Noodler, OSTRICH, cvc5, Z3-alpha, Z3-Noodler-Mocha-base, Z3-alpha-base, Z3-Noodler-base
UNSAT Performance Z3-Noodler-Mocha Z3-Noodler-Mocha, Z3-Noodler, OSTRICH, Z3-alpha, cvc5, Z3-Noodler-Mocha-base, Z3-Noodler-base, Z3-alpha-base
24 seconds Performance Z3-Noodler-Mocha Z3-Noodler-Mocha, Z3-Noodler, Z3-alpha, cvc5, OSTRICH, Z3-Noodler-Mocha-base, Z3-Noodler-base, Z3-alpha-base