SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

SMT-COMP 2025 Results - Incremental Track

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

Arith

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

Bitvec

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

Equality

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

Equality_LinearArith

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

Equality_MachineArith

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

Equality_NonLinearArith

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

FPArith

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

QF_Bitvec

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

QF_Equality

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

QF_Equality_Bitvec

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

QF_Equality_Bitvec_Arith

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

QF_Equality_LinearArith

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

QF_Equality_NonLinearArith

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

QF_FPArith

Scoring Scheme Winner Ranking
Parallel Performance Bitwuzla Bitwuzla, cvc5
SAT Performance -
UNSAT Performance -
24 seconds Performance Bitwuzla Bitwuzla, cvc5

QF_LinearIntArith

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

QF_LinearRealArith

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

QF_NonLinearIntArith

Scoring Scheme Winner Ranking
Parallel Performance Z3-Inc-Z3++ Z3-Inc-Z3++, SMTInterpol, cvc5, Yices2, Z3-Inc-Z3++-base
SAT Performance -
UNSAT Performance -
24 seconds Performance Yices2 Yices2, SMTInterpol, Z3-Inc-Z3++, cvc5, Z3-Inc-Z3++-base