SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

SMT-COMP 2020 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).

ANIA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incCVC4-inc, 2018-CVC4 (incremental)n, UltimateEliminator+MathSAT

AUFNIRA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-inc2019-CVC4-incn, CVC4-inc, z3n, UltimateEliminator+MathSAT

BV

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-inc2019-Z3n, CVC4-inc, z3n, UltimateEliminator+MathSAT

BVFP

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

LIA

Scoring SchemeWinnerRanking
Parallel PerformanceUltimateEliminator+MathSATz3n, 2018-Z3 (incremental)n, UltimateEliminator+MathSAT, CVC4-inc, SMTInterpol, SMTInterpol-fixedn

LRA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incCVC4-inc, UltimateEliminator+MathSAT, z3n, SMTInterpol-fixedn, SMTInterpol

QF_ABV

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, Yices2 incremental, 2018-Boolector (incremental)n, Yices2-fixed incrementaln, MathSAT5n, z3n, CVC4-inc

QF_ABVFP

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4-inc

QF_AUFBV

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incrementalYices2 incremental, Yices2-fixed incrementaln, 2019-Yices 2.6.2 Incrementaln, z3n, MathSAT5n, CVC4-inc, Bitwuzla, Bitwuzla-fixedn

QF_AUFLIA

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incremental2018-Yices (incremental)n, Yices2 incremental, Yices2-fixed incrementaln, z3n, SMTInterpol-fixedn, SMTInterpol, MathSAT5n, CVC4-inc

QF_BV

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incrementalYices2-fixed incrementaln, Yices2 incremental, 2019-Yices 2.6.2 Incrementaln, STP + CMS, Bitwuzla-fixedn, Bitwuzla, STP + MergeSAT, z3n, MathSAT5n, CVC4-inc, LazyBV2Int

QF_BVFP

The division has disagreements

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, MathSAT5n, CVC4-inc, z3n

QF_FP

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incCVC4-inc, Bitwuzla, Bitwuzla-fixedn, MathSAT5n, z3n

QF_LIA

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incrementalYices2-fixed incrementaln, 2018-Yices (incremental)n, Yices2 incremental, SMTInterpol, SMTInterpol-fixedn, MathSAT5n, CVC4-inc, z3n

QF_LRA

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incremental2018-MathSAT (incremental)n, MathSAT5n, Yices2-fixed incrementaln, Yices2 incremental, OpenSMT, SMTInterpol, SMTInterpol-fixedn, CVC4-inc, z3n

QF_NIA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incMathSAT5n, 2019-MathSAT-defaultn, CVC4-inc, z3n, Yices2-fixed incrementaln, Yices2 incremental

QF_UF

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incremental2019-Yices 2.6.2 Incrementaln, Yices2-fixed incrementaln, Yices2 incremental, z3n, CVC4-inc, SMTInterpol, SMTInterpol-fixedn, OpenSMT, MathSAT5n

QF_UFBV

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, 2018-Boolector (incremental)n, Yices2 incremental, Yices2-fixed incrementaln, z3n, MathSAT5n, CVC4-inc

QF_UFFP

Scoring SchemeWinnerRanking
Parallel PerformanceBitwuzlaBitwuzla-fixedn, Bitwuzla, CVC4-inc, MathSAT5n

QF_UFLIA

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incremental2018-Z3 (incremental)n, z3n, MathSAT5n, Yices2-fixed incrementaln, Yices2 incremental, SMTInterpol, SMTInterpol-fixedn, CVC4-inc

QF_UFLRA

Scoring SchemeWinnerRanking
Parallel PerformanceYices2 incrementalz3n, 2019-Z3n, MathSAT5n, Yices2 incremental, Yices2-fixed incrementaln, SMTInterpol, SMTInterpol-fixedn, CVC4-inc

QF_UFNIA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incMathSAT5n, 2019-MathSAT-defaultn, z3n, CVC4-inc, Yices2 incremental, Yices2-fixed incrementaln

UF

The division has disagreements

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incz3n, CVC4-inc, SMTInterpol, SMTInterpol-fixedn, UltimateEliminator+MathSAT

UFLRA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-inc2019-Z3n, z3n, CVC4-inc, SMTInterpol-fixedn, SMTInterpol, UltimateEliminator+MathSAT

UFNIA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incz3n, CVC4-inc, UltimateEliminator+MathSAT

UFNRA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incz3n, CVC4-inc, UltimateEliminator+MathSAT