SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

SMT-COMP 2025 Results - Model Validation Track

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

QF_ADT_BitVec

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

QF_ADT_LinArith

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

QF_Bitvec

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

QF_Datatypes

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

QF_Equality

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

QF_Equality_Bitvec

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

QF_Equality_LinearArith

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

QF_Equality_NonLinearArith

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

QF_FPArith

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

QF_LinearIntArith

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

QF_LinearRealArith

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

QF_NonLinearIntArith

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

QF_NonLinearRealArith

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