SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

SMT-COMP 2024 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 SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds PerformanceSMTInterpolSMTInterpol, cvc5

Bitvec

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, Bitwuzla, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds PerformanceBitwuzlaBitwuzla, cvc5, SMTInterpol

Equality

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, SMTInterpol

Equality_LinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, SMTInterpol

Equality_MachineArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, cvc5
SAT Performance-
UNSAT Performance-
24 seconds PerformanceBitwuzlaBitwuzla, cvc5

Equality_NonLinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, SMTInterpol

FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, cvc5
SAT Performance-
UNSAT Performance-
24 seconds Performancecvc5cvc5, Bitwuzla

QF_Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, Yices2, STP, cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds PerformanceSTPSTP, Yices2, Bitwuzla, SMTInterpol, cvc5

QF_Equality

Scoring SchemeWinnerRanking
Parallel PerformanceYices2Yices2, plat-smt, cvc5, SMTInterpol, OpenSMT
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, plat-smt, cvc5, SMTInterpol, OpenSMT

QF_Equality_Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, Yices2, cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, Bitwuzla, cvc5, SMTInterpol

QF_Equality_Bitvec_Arith

Scoring SchemeWinnerRanking
Parallel PerformanceYices2Yices2, cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, cvc5, SMTInterpol

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpolSMTInterpol, cvc5, Yices2, OpenSMT
SAT Performance-
UNSAT Performance-
24 seconds PerformanceYices2Yices2, SMTInterpol, cvc5, OpenSMT

QF_Equality_NonLinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5cvc5, SMTInterpol, Yices2
SAT Performance-
UNSAT Performance-
24 seconds PerformanceSMTInterpolSMTInterpol, cvc5, Yices2

QF_FPArith

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla, cvc5
SAT Performance-
UNSAT Performance-
24 seconds PerformanceBitwuzlaBitwuzla, cvc5

QF_LinearIntArith

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

QF_LinearRealArith

Scoring SchemeWinnerRanking
Parallel PerformanceOpenSMTOpenSMT, Yices2, cvc5, SMTInterpol
SAT Performance-
UNSAT Performance-
24 seconds Performance-

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpolSMTInterpol, cvc5, Yices2
SAT Performance-
UNSAT Performance-
24 seconds Performance-