SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

SMT-COMP 2021 Results - Incremental Track (Summary)

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 Performancecvc5-inccvc5-inc, 2020-CVC4-incn, UltimateEliminator+MathSAT, 2020-z3n, z3n, SMTInterpol

Bitvec

Scoring SchemeWinnerRanking
Parallel Performancecvc5-inc2019-Z3n, z3n, cvc5-inc, UltimateEliminator+MathSAT

Equality+LinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5-incz3n, 2020-z3n, 2019-Z3n, cvc5-inc, SMTInterpol, UltimateEliminator+MathSAT

Equality+NonLinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5-inc2020-z3n, z3n, cvc5-inc, 2020-CVC4-incn, SMTInterpol, UltimateEliminator+MathSAT, 2019-CVC4-incn

Equality

Scoring SchemeWinnerRanking
Parallel Performancecvc5-inc2020-z3n, z3n, cvc5-inc, SMTInterpol, UltimateEliminator+MathSAT

FPArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5-inc2019-CVC4-incn, cvc5-inc, UltimateEliminator+MathSAT

QF_Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceSTPSTP, 2020-Yices2-fixed incrementaln, MathSAT5n, Yices2 incremental, cvc5-inc, Bitwuzla, z3n

QF_Equality+Bitvec

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incremental2020-Yices2 incrementaln, Yices2 incremental, MathSAT5n, Bitwuzla, 2020-Bitwuzla-fixedn, cvc5-inc, z3n

QF_Equality+LinearArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5-inc2020-z3n, z3n, cvc5-inc, SMTInterpol, 2018-Yices (incremental)n, Yices2 incremental, MathSAT5n, 2018-Z3 (incremental)n

QF_Equality+NonLinearArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpolz3n, SMTInterpol, cvc5-inc, 2020-MathSAT5n, MathSAT5n, Yices2 incremental

QF_Equality

Scoring SchemeWinnerRanking
Parallel Performancecvc5-incz3n, cvc5-inc, SMTInterpol, 2019-Yices 2.6.2 Incrementaln, Yices2 incremental, OpenSMT, MathSAT5n

QF_FPArith

Scoring SchemeWinnerRanking
Parallel Performancecvc5-incBitwuzla - fixedn, 2020-Bitwuzla-fixedn, cvc5-inc, 2020-CVC4-incn, z3n, MathSAT5n, Bitwuzla

QF_LinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incrementalYices2 incremental, 2020-Yices2-fixed incrementaln, z3n, MathSAT5n, SMTInterpol, cvc5-inc, OpenSMT

QF_LinearRealArith

Scoring SchemeWinnerRanking
Parallel PerformanceOpenSMT2018-MathSAT (incremental)n, MathSAT5n, OpenSMT, Yices2 incremental, cvc5-inc, SMTInterpol, z3n

QF_NonLinearIntArith

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpolMathSAT5n, 2020-MathSAT5n, z3n, SMTInterpol, cvc5-inc, Yices2 incremental