SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

SMT-COMP 2025 Results - Unsat Core Track

Summary of all competition results for the Unsat Core 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 cvc5 cvc5, SMTInterpol, UltimateEliminator+MathSAT
Parallel Performance cvc5 cvc5, SMTInterpol, UltimateEliminator+MathSAT
SAT Performance -
UNSAT Performance cvc5 cvc5, SMTInterpol, UltimateEliminator+MathSAT
24 seconds Performance cvc5 cvc5, SMTInterpol, UltimateEliminator+MathSAT

Bitvec

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

Equality

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

Equality_LinearArith

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

Equality_MachineArith

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

FPArith

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

QF_Bitvec

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

QF_Datatypes

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

QF_Equality

Scoring Scheme Winner Ranking
Sequential Performance Yices2 Yices2, SMTInterpol, cvc5, OpenSMT (min-ucore), OpenSMT
Parallel Performance Yices2 Yices2, SMTInterpol, cvc5, OpenSMT (min-ucore), OpenSMT
SAT Performance -
UNSAT Performance Yices2 Yices2, SMTInterpol, cvc5, OpenSMT (min-ucore), OpenSMT
24 seconds Performance Yices2 Yices2, SMTInterpol, cvc5, OpenSMT (min-ucore), OpenSMT

QF_Equality_Bitvec

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

QF_Equality_LinearArith

Scoring Scheme Winner Ranking
Sequential Performance Yices2 Yices2, cvc5, SMTInterpol, OpenSMT (min-ucore), OpenSMT
Parallel Performance Yices2 Yices2, cvc5, SMTInterpol, OpenSMT (min-ucore), OpenSMT
SAT Performance -
UNSAT Performance Yices2 Yices2, cvc5, SMTInterpol, OpenSMT (min-ucore), OpenSMT
24 seconds Performance Yices2 Yices2, cvc5, SMTInterpol, OpenSMT (min-ucore), OpenSMT

QF_Equality_NonLinearArith

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

QF_FPArith

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

QF_LinearIntArith

Scoring Scheme Winner Ranking
Sequential Performance Yices2 Yices2, SMTInterpol, cvc5, OpenSMT (min-ucore), OpenSMT
Parallel Performance Yices2 Yices2, SMTInterpol, cvc5, OpenSMT (min-ucore), OpenSMT
SAT Performance -
UNSAT Performance Yices2 Yices2, SMTInterpol, cvc5, OpenSMT (min-ucore), OpenSMT
24 seconds Performance Yices2 Yices2, cvc5, SMTInterpol, OpenSMT (min-ucore), OpenSMT

QF_LinearRealArith

Scoring Scheme Winner Ranking
Sequential Performance OpenSMT OpenSMT, OpenSMT (min-ucore), Yices2, cvc5, SMTInterpol
Parallel Performance OpenSMT OpenSMT, OpenSMT (min-ucore), Yices2, cvc5, SMTInterpol
SAT Performance -
UNSAT Performance OpenSMT OpenSMT, OpenSMT (min-ucore), Yices2, cvc5, SMTInterpol
24 seconds Performance Yices2 Yices2, OpenSMT, OpenSMT (min-ucore), cvc5, SMTInterpol

QF_NonLinearIntArith

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

QF_NonLinearRealArith

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