SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

SMT-COMP 2024 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 SchemeWinnerRanking
Sequential Performancecvc5cvc5, YicesQS, SMTInterpol, SMT-RAT, iProver v3.9, Amaya
Parallel Performancecvc5cvc5, YicesQS, SMTInterpol, SMT-RAT, iProver v3.9, Amaya
SAT PerformanceYicesQSYicesQS, cvc5, SMTInterpol, SMT-RAT, iProver v3.9, Amaya
UNSAT Performancecvc5cvc5, YicesQS, iProver v3.9, SMTInterpol, SMT-RAT, Amaya
24 seconds PerformanceYicesQSYicesQS, cvc5, SMTInterpol, SMT-RAT, iProver v3.9, Amaya

Bitvec

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, YicesQS, Bitwuzla, Z3-alpha, SMTInterpol
Parallel Performancecvc5cvc5, YicesQS, Bitwuzla, Z3-alpha, SMTInterpol
SAT PerformanceBitwuzlaBitwuzla, cvc5, YicesQS, Z3-alpha, SMTInterpol
UNSAT Performancecvc5cvc5, YicesQS, Bitwuzla, Z3-alpha, SMTInterpol
24 seconds PerformanceYicesQSYicesQS, Bitwuzla, Z3-alpha, cvc5, SMTInterpol

Equality

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, iProver v3.9, SMTInterpol, Yices2
Parallel Performancecvc5cvc5, iProver v3.9, SMTInterpol, Yices2
SAT Performancecvc5cvc5, iProver v3.9, Yices2, SMTInterpol
UNSAT Performancecvc5cvc5, iProver v3.9, SMTInterpol, Yices2
24 seconds Performancecvc5cvc5, iProver v3.9, Yices2, SMTInterpol

Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, iProver v3.9, SMTInterpol
Parallel Performancecvc5cvc5, iProver v3.9, SMTInterpol
SAT Performancecvc5cvc5, SMTInterpol, iProver v3.9
UNSAT Performancecvc5cvc5, iProver v3.9, SMTInterpol
24 seconds Performancecvc5cvc5, SMTInterpol, iProver v3.9

Equality_MachineArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, Bitwuzla, SMTInterpol
Parallel Performancecvc5cvc5, Bitwuzla, SMTInterpol
SAT Performancecvc5cvc5, Bitwuzla, SMTInterpol
UNSAT Performancecvc5cvc5, SMTInterpol, Bitwuzla
24 seconds Performancecvc5cvc5, Bitwuzla, SMTInterpol

Equality_NonLinearArith

Scoring SchemeWinnerRanking
Sequential Performancecvc5cvc5, iProver v3.9, SMTInterpol
Parallel Performancecvc5cvc5, SMTInterpol, iProver v3.9
SAT Performancecvc5cvc5, SMTInterpol, iProver v3.9
UNSAT Performancecvc5cvc5, iProver v3.9, SMTInterpol
24 seconds Performancecvc5cvc5, iProver v3.9, SMTInterpol

FPArith

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, cvc5
Parallel PerformanceBitwuzlaBitwuzla, cvc5
SAT PerformanceBitwuzlaBitwuzla, cvc5
UNSAT PerformanceBitwuzlaBitwuzla, cvc5
24 seconds PerformanceBitwuzlaBitwuzla, cvc5

QF_Bitvec

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

QF_Datatypes

Scoring SchemeWinnerRanking
Sequential PerformanceAlgarobaAlgaroba, cvc5, Z3-alpha, SMTInterpol
Parallel PerformanceAlgarobaAlgaroba, cvc5, Z3-alpha, SMTInterpol
SAT Performancecvc5cvc5, Algaroba, Z3-alpha, SMTInterpol
UNSAT PerformanceZ3-alphaZ3-alpha, Algaroba, cvc5, SMTInterpol
24 seconds PerformanceAlgarobaAlgaroba, SMTInterpol, cvc5, Z3-alpha

QF_Equality

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, Z3-alpha, cvc5, OpenSMT, SMTInterpol, plat-smt
Parallel PerformanceYices2Yices2, Z3-alpha, cvc5, OpenSMT, SMTInterpol, plat-smt
SAT PerformanceYices2Yices2, OpenSMT, Z3-alpha, cvc5, SMTInterpol, plat-smt
UNSAT PerformanceYices2Yices2, Z3-alpha, cvc5, OpenSMT, SMTInterpol, plat-smt
24 seconds PerformanceYices2Yices2, Z3-alpha, OpenSMT, cvc5, SMTInterpol, plat-smt

QF_Equality_Bitvec

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, Yices2, SMTInterpol, Z3-alpha, cvc5
Parallel PerformanceBitwuzlaBitwuzla, Yices2, SMTInterpol, Z3-alpha, cvc5
SAT PerformanceBitwuzlaBitwuzla, Yices2, cvc5, SMTInterpol, Z3-alpha
UNSAT PerformanceBitwuzlaBitwuzla, Yices2, SMTInterpol, Z3-alpha, cvc5
24 seconds PerformanceYices2Yices2, Bitwuzla, cvc5, SMTInterpol, Z3-alpha

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceSMTInterpolSMTInterpol, OpenSMT, cvc5, Yices2
Parallel PerformanceSMTInterpolSMTInterpol, OpenSMT, cvc5, Yices2
SAT PerformanceSMTInterpolSMTInterpol, OpenSMT, cvc5, Yices2
UNSAT PerformanceOpenSMTOpenSMT, Yices2, cvc5, SMTInterpol
24 seconds PerformanceYices2Yices2, SMTInterpol, OpenSMT, cvc5

QF_Equality_NonLinearArith

Scoring SchemeWinnerRanking
Sequential PerformanceYices2Yices2, cvc5, SMTInterpol
Parallel PerformanceYices2Yices2, cvc5, SMTInterpol
SAT PerformanceYices2Yices2, cvc5, SMTInterpol
UNSAT Performancecvc5cvc5, Yices2, SMTInterpol
24 seconds PerformanceYices2Yices2, cvc5, SMTInterpol

QF_FPArith

Scoring SchemeWinnerRanking
Sequential PerformanceBitwuzlaBitwuzla, cvc5, COLIBRI
Parallel PerformanceBitwuzlaBitwuzla, cvc5, COLIBRI
SAT PerformanceBitwuzlaBitwuzla, cvc5, COLIBRI
UNSAT PerformanceBitwuzlaBitwuzla, cvc5, COLIBRI
24 seconds PerformanceBitwuzlaBitwuzla, COLIBRI, cvc5

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceOpenSMTOpenSMT, cvc5, Yices2, Z3-alpha, SMTInterpol
Parallel PerformanceOpenSMTOpenSMT, cvc5, Yices2, Z3-alpha, SMTInterpol
SAT PerformanceZ3-alphaZ3-alpha, OpenSMT, Yices2, cvc5, SMTInterpol
UNSAT Performancecvc5cvc5, OpenSMT, Yices2, SMTInterpol, Z3-alpha
24 seconds PerformanceYices2Yices2, Z3-alpha, OpenSMT, cvc5, SMTInterpol

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceOpenSMTOpenSMT, Yices2, cvc5, Z3-alpha, SMTInterpol
Parallel PerformanceOpenSMTOpenSMT, Yices2, cvc5, Z3-alpha, SMTInterpol
SAT PerformanceOpenSMTOpenSMT, Yices2, Z3-alpha, cvc5, SMTInterpol
UNSAT Performancecvc5cvc5, Z3-alpha, OpenSMT, Yices2, SMTInterpol
24 seconds PerformanceYices2Yices2, OpenSMT, Z3-alpha, cvc5, SMTInterpol

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Sequential PerformanceZ3-alphaZ3-alpha, Yices2, cvc5, SMTInterpol
Parallel PerformanceZ3-alphaZ3-alpha, Yices2, cvc5, SMTInterpol
SAT PerformanceZ3-alphaZ3-alpha, cvc5, Yices2, SMTInterpol
UNSAT PerformanceZ3-alphaZ3-alpha, Yices2, cvc5, SMTInterpol
24 seconds PerformanceYices2Yices2, Z3-alpha, cvc5, SMTInterpol

QF_NonLinearRealArith

Scoring SchemeWinnerRanking
Sequential PerformanceZ3-alphaZ3-alpha, cvc5, Yices2, SMT-RAT, SMTInterpol
Parallel PerformanceZ3-alphaZ3-alpha, cvc5, Yices2, SMT-RAT, SMTInterpol
SAT PerformanceZ3-alphaZ3-alpha, Yices2, cvc5, SMT-RAT, SMTInterpol
UNSAT Performancecvc5cvc5, Z3-alpha, Yices2, SMT-RAT, SMTInterpol
24 seconds PerformanceYices2Yices2, cvc5, Z3-alpha, SMT-RAT, SMTInterpol

QF_Strings

Scoring SchemeWinnerRanking
Sequential PerformanceZ3-NoodlerZ3-Noodler, cvc5, Z3-alpha, OSTRICH
Parallel PerformanceZ3-NoodlerZ3-Noodler, cvc5, Z3-alpha, OSTRICH
SAT PerformanceZ3-NoodlerZ3-Noodler, cvc5, Z3-alpha, OSTRICH
UNSAT PerformanceZ3-NoodlerZ3-Noodler, OSTRICH, Z3-alpha, cvc5
24 seconds PerformanceZ3-NoodlerZ3-Noodler, Z3-alpha, cvc5, OSTRICH