SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

SMT-COMP 2024 Results - Cloud Track

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

QF_Equality_LinearArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceSMTSSMTS, cvc5-cloud
SAT PerformanceSMTSSMTS, cvc5-cloud
UNSAT PerformanceSMTSSMTS, cvc5-cloud
24 seconds PerformanceSMTSSMTS

QF_LinearIntArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceSMTSSMTS, Z3-Parti-Z3++, cvc5-cloud
SAT PerformanceSMTSSMTS, Z3-Parti-Z3++, cvc5-cloud
UNSAT PerformanceZ3-Parti-Z3++Z3-Parti-Z3++, SMTS, cvc5-cloud
24 seconds PerformanceSMTSSMTS, Z3-Parti-Z3++, cvc5-cloud

QF_LinearRealArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceSMTSSMTS, Z3-Parti-Z3++, cvc5-cloud
SAT PerformanceSMTSSMTS, Z3-Parti-Z3++, cvc5-cloud
UNSAT PerformanceSMTSSMTS, Z3-Parti-Z3++, cvc5-cloud
24 seconds PerformanceSMTSSMTS, Z3-Parti-Z3++, cvc5-cloud

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceZ3-Parti-Z3++Z3-Parti-Z3++, cvc5-cloud
SAT PerformanceZ3-Parti-Z3++Z3-Parti-Z3++, cvc5-cloud
UNSAT PerformanceZ3-Parti-Z3++Z3-Parti-Z3++, cvc5-cloud
24 seconds PerformanceZ3-Parti-Z3++Z3-Parti-Z3++

QF_NonLinearRealArith

Scoring SchemeWinnerRanking
Sequential Performance-
Parallel PerformanceZ3-Parti-Z3++Z3-Parti-Z3++, cvc5-cloud
SAT PerformanceZ3-Parti-Z3++Z3-Parti-Z3++, cvc5-cloud
UNSAT Performancecvc5-cloudcvc5-cloud, Z3-Parti-Z3++
24 seconds PerformanceZ3-Parti-Z3++Z3-Parti-Z3++, cvc5-cloud