SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

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

ABVFP

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incCVC4-inc, UltimateEliminator+MathSAT-5.5.4, Z3n

ALIA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-inc2018-Z3 (incremental)n, Z3n, CVC4-inc, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

ANIA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-inc2018-CVC4 (incremental)n, CVC4-inc, Z3n, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

AUFNIRA

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

BV

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incZ3n, CVC4-inc, 2018-Z3 (incremental)n, UltimateEliminator+MathSAT-5.5.4, Q3B

BVFP

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incCVC4-inc, UltimateEliminator+MathSAT-5.5.4, Z3n

LIA

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpol2018-Z3 (incremental)n, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, CVC4-inc, UltimateEliminator+Yices-2.6.1

LRA

Scoring SchemeWinnerRanking
Parallel Performance-CVC4-inc, Z3n, SMTInterpol, UltimateEliminator+SMTInterpol, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1

QF_ABV

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 Incremental2018-Boolector (incremental)n, Yices 2.6.2 Incremental, Boolector (incremental), CVC4-inc, Z3n

QF_ALIA

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpol2018-Z3 (incremental)n, Z3n, SMTInterpol, Yices 2.6.2 Incremental, CVC4-inc

QF_ANIA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-inc2018-Z3 (incremental)n, Z3n, CVC4-inc, MathSAT-default, MathSAT-na-ext

QF_AUFBV

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 IncrementalYices 2.6.2 Incremental, 2018-Yices (incremental)n, Z3n, CVC4-inc, Boolector (incremental)

QF_AUFBVNIA

Scoring SchemeWinnerRanking
Parallel PerformanceMathSAT-na-extMathSAT-na-ext, MathSAT-default, CVC4-inc, Z3n

QF_AUFLIA

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 Incremental2018-Yices (incremental)n, Yices 2.6.2 Incremental, Z3n, SMTInterpol, CVC4-inc

QF_BV

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 IncrementalYices 2.6.2 Incremental, Minkeyrink Solver MT, Minkeyrink Solver, 2018-MathSAT (incremental)n, STP-incremental, Boolector (incremental), CVC4-inc-fixedn, Z3n, STP-mt, Boolector-ReasonLSn, CVC4-inc

QF_LIA

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 Incremental2018-Yices (incremental)n, Yices 2.6.2 Incremental, Z3n, SMTInterpol, CVC4-inc-fixedn, CVC4-inc

QF_LRA

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 Incremental2018-MathSAT (incremental)n, Yices 2.6.2 Incremental, CVC4-inc, SMTInterpol, Z3n

QF_NIA

Scoring SchemeWinnerRanking
Parallel PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, 2018-CVC4 (incremental)n, CVC4-inc, Z3n, Yices 2.6.2 Incremental

QF_UF

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 IncrementalYices 2.6.2 Incremental, Z3n, CVC4-inc, SMTInterpol

QF_UFBV

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 Incremental2018-Boolector (incremental)n, Yices 2.6.2 Incremental, Boolector (incremental), Z3n, CVC4-inc

QF_UFLIA

Scoring SchemeWinnerRanking
Parallel PerformanceSMTInterpol2018-Z3 (incremental)n, Z3n, SMTInterpol, CVC4-inc, Yices 2.6.2 Incremental

QF_UFLRA

Scoring SchemeWinnerRanking
Parallel PerformanceYices 2.6.2 IncrementalZ3n, 2018-Z3 (incremental)n, Yices 2.6.2 Incremental, CVC4-inc, SMTInterpol

QF_UFNIA

Scoring SchemeWinnerRanking
Parallel PerformanceMathSAT-defaultMathSAT-default, MathSAT-na-ext, Z3n, 2018-Z3 (incremental)n, CVC4-inc, Yices 2.6.2 Incremental

UFLRA

Scoring SchemeWinnerRanking
Parallel PerformanceCVC4-incZ3n, CVC4-inc, SMTInterpol, 2018-Z3 (incremental)n, UltimateEliminator+MathSAT-5.5.4, UltimateEliminator+Yices-2.6.1, UltimateEliminator+SMTInterpol