SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

SMT-COMP 2022 Results - Cloud Track (Summary)

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).
This track is experimental. Solvers are only ranked by performance, but no winner is selected.

Arith

Scoring SchemeRanking
Parallel PerformanceVampire, cvc5-cloud
SAT Performancecvc5-cloud, Vampire
UNSAT PerformanceVampire, cvc5-cloud
24s PerformanceVampire, cvc5-cloud

Equality+LinearArith

Scoring SchemeRanking
Parallel PerformanceVampire, cvc5-cloud
SAT Performancecvc5-cloud, Vampire
UNSAT PerformanceVampire, cvc5-cloud
24s Performancecvc5-cloud, Vampire

Equality+NonLinearArith

Scoring SchemeRanking
Parallel PerformanceVampire, cvc5-cloud
SAT Performancecvc5-cloud, Vampire
UNSAT PerformanceVampire, cvc5-cloud
24s PerformanceVampire, cvc5-cloud

Equality

Scoring SchemeRanking
Parallel PerformanceVampire, cvc5-cloud
SAT PerformanceVampire, cvc5-cloud
UNSAT PerformanceVampire, cvc5-cloud
24s PerformanceVampire, cvc5-cloud

QF_Equality+LinearArith

Scoring SchemeRanking
Parallel PerformanceSMTS portfolio, SMTS cube-and-conquer, SMTS cube-and-conquer (fixed), cvc5-cloud
SAT PerformanceSMTS portfolio, SMTS cube-and-conquer, SMTS cube-and-conquer (fixed), cvc5-cloud
UNSAT PerformanceSMTS cube-and-conquer, SMTS cube-and-conquer (fixed), SMTS portfolio, cvc5-cloud
24s PerformanceSMTS cube-and-conquer, SMTS cube-and-conquer (fixed), SMTS portfolio, cvc5-cloud

QF_LinearIntArith

Scoring SchemeRanking
Parallel PerformanceSMTS cube-and-conquer (fixed), SMTS portfolio, cvc5-cloud, SMTS cube-and-conquer
SAT PerformanceSMTS cube-and-conquer (fixed), SMTS portfolio, SMTS cube-and-conquer, cvc5-cloud
UNSAT Performancecvc5-cloud, SMTS cube-and-conquer (fixed), SMTS cube-and-conquer, SMTS portfolio
24s Performancecvc5-cloud, SMTS portfolio, SMTS cube-and-conquer (fixed), SMTS cube-and-conquer

QF_LinearRealArith

Scoring SchemeRanking
Parallel PerformanceSMTS portfolio, SMTS cube-and-conquer, SMTS cube-and-conquer (fixed), cvc5-cloud
SAT PerformanceSMTS portfolio, SMTS cube-and-conquer (fixed), SMTS cube-and-conquer, cvc5-cloud
UNSAT PerformanceSMTS portfolio, SMTS cube-and-conquer, SMTS cube-and-conquer (fixed), cvc5-cloud
24s PerformanceSMTS portfolio, SMTS cube-and-conquer, cvc5-cloud, SMTS cube-and-conquer (fixed)