SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Biggest Lead Ranking- Single Query Track

Page generated on 2019-07-23 17:56:11 +0000

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
CVC4 CVC4 CVC4 CVC4 CVC4

Sequential Performance

Solver Correct Score Time Score Division
CVC4 4.81111111 0.00641507 FP
CVC4 4.5 0.00215211 BVFP
CVC4 3.12857143 1.92536585 UFDTLIA
CVC4 2.5 33.6783498 QF_DT
CVC4 2.15 10048.81148573 LIA
CVC4 2.0 1.02285697 ABVFP
Par4 1.79310345 1.66034842 UFBV
CVC4 1.51648352 2.41786319 AUFDTLIA
SMT-RAT 1.5 4.99807645 QF_NIRA
CVC4 1.27884615 1.11254713 UFDT
Par4 1.2 2.48242549 QF_NRA
Par4 1.18181818 0.97855922 UFIDL
Yices 2.6.2 1.18181818 0.00229715 QF_AUFBV
Par4 1.15441176 2.75008305 LRA
Par4 1.14285714 11.03552619 QF_LIRA
CVC4 1.11111111 4272.273168 NIA
Par4 1.08226779 1.3569919 QF_NIA
Par4 1.06779661 0.97384688 AUFNIRA
Par4 1.05728068 1.05005047 UFNIA
CVC4 1.05535055 28.05025968 QF_UFNIA
SMTInterpol 1.05263158 0.00525195 ALIA
Par4 1.04819277 1.50696843 NRA
Par4 1.04613297 1.44363117 BV
Yices 2.6.2 1.04545455 9.25424924 QF_UFIDL
Par4 1.04 1.85014286 QF_UFNRA
Par4 1.03045685 0.98625872 QF_FP
Par4 1.02626521 1.52033074 AUFLIRA
Par4 1.01823708 1.00130611 UFLIA
SPASS-SATT 1.01734104 1.79357266 QF_LRA
Yices 2.6.2 1.01415094 1.14506797 QF_RDL
Yices 2.6.2 1.01376147 1.33232799 QF_UFBV
CVC4 1.01151461 1.03834322 UF
Par4 1.00787143 1.4268963 QF_LIA
CVC4 1.00436047 1.05905335 AUFLIA
Boolector 1.00378484 1.11309434 QF_BV
Yices 2.6.2 1.00216685 1.04617415 QF_IDL
Par4 1.00193798 1.13428816 QF_BVFP
SMTInterpol 1.00184843 0.55141036 QF_UFLRA
Boolector 1.00026599 1.04208793 QF_ABV
Yices 2.6.2 1.0 38.87493121 QF_AUFLIA
Yices 2.6.2 1.0 14.46422789 QF_ALIA
Yices 2.6.2 1.0 14.04681274 QF_AX
Yices 2.6.2 1.0 9.8631481 QF_UFLIA
Vampire 1.0 5.86968221 UFDTNIA
Alt-Ergo 1.0 1.71205839 UFLRA
Yices 2.6.2 1.0 1.14636635 QF_UF
MathSAT-default 1.0 1.03226779 QF_AUFNIA
CVC4 1.0 1.00811499 QF_ANIA

Parallel Performance

Solver Correct Score Time Score Division
CVC4 4.81111111 0.00447263 FP
CVC4 4.5 0.00152223 BVFP
CVC4 3.12857143 1.83818588 UFDTLIA
CVC4 2.5 8.5288138 QF_DT
CVC4 2.13475177 10017.21134053 LIA
CVC4 2.0 0.79152982 ABVFP
Par4 1.79310345 1.67832347 UFBV
CVC4 1.50819672 4.82722907 AUFDTLIA
SMT-RAT 1.5 4.99903356 QF_NIRA
CVC4 1.22298851 1.05657445 UFDT
Par4 1.2073903 2.80195541 QF_NRA
Par4 1.18181818 1.02683494 UFIDL
Yices 2.6.2 1.18181818 0.0022979 QF_AUFBV
Par4 1.17647059 3.38671151 LRA
Par4 1.14285714 21.82635679 QF_LIRA
CVC4 1.11111111 4243.98375642 NIA
Par4 1.09589867 1.5291578 QF_NIA
Par4 1.08474576 1.01894077 AUFNIRA
Par4 1.08 2.9566771 QF_UFNRA
Par4 1.06598985 1.14984214 QF_FP
Par4 1.06024096 1.61563749 NRA
Par4 1.05939102 1.12243517 UFNIA
CVC4 1.05535055 28.04640858 QF_UFNIA
SMTInterpol 1.05263158 0.00585711 ALIA
Par4 1.04851752 1.60618234 BV
Yices 2.6.2 1.04545455 8.92896488 QF_UFIDL
Par4 1.02429668 1.53272178 AUFLIRA
Par4 1.0224924 1.03986353 UFLIA
Par4 1.02162162 1.14922164 QF_IDL
Par4 1.01515152 1.28978682 QF_LRA
Yices 2.6.2 1.01415094 1.14395362 QF_RDL
Vampire 1.01312336 1.03368881 UF
Par4 1.0124631 1.85394731 QF_LIA
Yices 2.6.2 1.00913242 1.25215804 QF_UFBV
Poolector 1.00194241 1.11862612 QF_BV
Par4 1.00193798 3.16108631 QF_BVFP
SMTInterpol 1.00184843 0.79765227 QF_UFLRA
Vampire 1.00072359 1.0009835 AUFLIA
Yices 2.6.2 1.0 22.64972968 QF_AUFLIA
Yices 2.6.2 1.0 12.42317995 QF_AX
Yices 2.6.2 1.0 9.79847656 QF_UFLIA
Yices 2.6.2 1.0 7.03463218 QF_ALIA
Vampire 1.0 5.30200722 UFDTNIA
Alt-Ergo 1.0 1.87303031 UFLRA
Par4 1.0 1.18614545 QF_ABV
Par4 1.0 1.10943015 QF_UF
MathSAT-default 1.0 1.0322563 QF_AUFNIA
CVC4 1.0 1.00797504 QF_ANIA

SAT Performance

Solver Correct Score Time Score Division
CVC4 94.0 2.16182831 AUFDTLIA
Par4 55.0 0.04979824 AUFLIRA
Par4 19.0 318.42781427 UFBV
CVC4 11.0 0.00202615 FP
CVC4 5.0 9096.34230476 LIA
CVC4 4.0 1.06170356 QF_DT
CVC4 2.5 0.00126837 BVFP
CVC4 2.03389831 1.28786949 UFDT
Par4 2.0 3187.75274605 AUFNIRA
Par4 2.0 1.9640133 UFIDL
SMTInterpol 2.0 0.8027683 ALIA
CVC4 2.0 0.79152982 ABVFP
Par4 2.0 0.00242394 NRA
Par4 1.5 1.06253514 UFLIA
CVC4 1.38 3.35380259 AUFLIA
Par4 1.19808307 11.08600635 LRA
Par4 1.14915572 2.49953682 QF_NRA
Yices 2.6.2 1.14285714 0.00489222 QF_AUFBV
Vampire 1.13527851 5.89801793 UF
CVC4 1.125 3265.23826828 NIA
Par4 1.08910891 1.71929576 QF_FP
Par4 1.08695652 2.95647637 QF_UFNRA
Par4 1.07673695 2.6029153 QF_NIA
CVC4 1.02923977 9.18697202 QF_UFNIA
Par4 1.02422145 1.49630019 QF_LRA
Par4 1.01672241 1.18130481 QF_IDL
Par4 1.01458576 2.00653059 QF_LIA
Yices 2.6.2 1.00952381 12.29114174 QF_RDL
Par4 1.00442478 0.92054301 BV
SMTInterpol 1.0030303 0.92446268 QF_UFLRA
Poolector 1.00227865 1.21616366 QF_BV
Yices 2.6.2 1.0 15.06119143 QF_UFLIA
Yices 2.6.2 1.0 9.46471539 QF_AUFLIA
Yices 2.6.2 1.0 4.0817612 QF_UFBV
Yices 2.6.2 1.0 3.48240527 QF_AX
Yices 2.6.2 1.0 3.43908462 QF_ALIA
Par4 1.0 3.35027139 QF_BVFP
Poolector 1.0 2.15817325 QF_ABV
Yices 2.6.2 1.0 2.15658298 QF_UFIDL
Par4 1.0 1.78576496 UFNIA
Yices 2.6.2 1.0 1.22449141 QF_LIRA
Yices 2.6.2 1.0 1.1120863 QF_UF
MathSAT-default 1.0 1.10889061 QF_AUFNIA

UNSAT Performance

Solver Correct Score Time Score Division
CVC4 5.0 3.06355873 BVFP
CVC4 4.75555556 0.00896692 FP
CVC4 3.12857143 3.31099902 UFDTLIA
SMT-RAT 1.5 4.99903356 QF_NIRA
Yices 2.6.2 1.18518519 0.00234983 QF_AUFBV
Par4 1.17241379 360.82669031 UFBV
Par4 1.16666667 21.88861118 QF_LIRA
Par4 1.16269841 3.90200456 LRA
Par4 1.12175962 3.47171685 QF_NIA
Par4 1.11916264 7.91511719 QF_NRA
CVC4 1.10144928 4566.76815779 LIA
CVC4 1.09549072 1.79515715 UFDT
Par4 1.06883298 1.25565582 UFNIA
Yices 2.6.2 1.06190476 8.91819014 QF_UFIDL
Par4 1.05172414 1.454249 AUFNIRA
Par4 1.04819277 1.55017344 NRA
Par4 1.03370787 2.61505077 BV
Vampire 1.0313253 3.25860169 AUFLIA
Par4 1.03061224 1.04892613 QF_FP
Yices 2.6.2 1.02325581 1.23058221 QF_UFBV
Par4 1.02073171 1.90929036 UFLIA
Par4 1.01807229 1.22440862 QF_IDL
Par4 1.00973054 2.39452735 QF_LIA
Yices 2.6.2 1.00917431 1.95363961 QF_RDL
Par4 1.00913838 1.28721612 UF
Par4 1.00416667 1.16456233 QF_LRA
Par4 1.00347222 3.10756232 QF_BVFP
Vampire 1.00192184 1.27218327 AUFLIRA
Poolector 1.00176025 1.12574992 QF_BV
Par4 1.00042355 1.15212129 QF_ABV
CVC4 1.0 2664.41936221 QF_UFNIA
CVC4 1.0 1985.25561652 NIA
CVC4 1.0 184.65867701 AUFDTLIA
Yices 2.6.2 1.0 31.27145866 QF_ALIA
Yices 2.6.2 1.0 24.10694354 QF_AUFLIA
Yices 2.6.2 1.0 15.31843472 QF_AX
CVC4 1.0 8.54098957 QF_DT
Yices 2.6.2 1.0 7.94785762 QF_UFLIA
Vampire 1.0 5.30200722 UFDTNIA
Yices 2.6.2 1.0 3.33251429 QF_UFLRA
Par4 1.0 1.38836051 UFIDL
Par4 1.0 1.14893569 QF_UF
veriT 1.0 1.00943057 UFLRA
CVC4 1.0 1.00797504 QF_ANIA
Alt-Ergo 1.0 1.00791386 ALIA
MathSAT-default 1.0 1.0049441 QF_UFNRA
MathSAT-na-ext 1.0 1.00265313 QF_AUFNIA

24s Performance

Solver Correct Score Time Score Division
CVC4 4.5 0.14975966 BVFP
CVC4 4.37222222 0.29792131 FP
CVC4 4.0 1.00259373 QF_DT
Par4 3.71428571 2.36646389 UFBV
CVC4 2.18115942 104.63617539 LIA
CVC4 2.0 0.79152982 ABVFP
Par4 1.9 1.63850588 QF_UFNRA
CVC4 1.42857143 77.06188252 NIA
CVC4 1.28813559 0.99959185 AUFDTLIA
Par4 1.22247706 1.28171455 QF_NIA
Par4 1.20851064 1.63563486 LRA
Par4 1.20488534 1.6435542 QF_NRA
Par4 1.2 1.00509534 UFIDL
Par4 1.19621555 1.16316342 UFNIA
Par4 1.18473101 4.02031041 QF_LIA
Yices 2.6.2 1.15976331 1.56749612 QF_RDL
Yices 2.6.2 1.14785992 6.58728152 QF_UFIDL
Vampire 1.09385113 1.25913638 AUFLIA
Par4 1.0931677 1.12840006 UFLIA
Vampire 1.09259259 1.00773373 UFDTLIA
Yices 2.6.2 1.09090909 0.10354564 QF_AUFBV
Par4 1.08860759 2.07150996 NRA
Vampire 1.07788595 0.99247831 UF
Par4 1.07142857 1.04568879 AUFNIRA
CVC4 1.06367041 4.70889794 QF_UFNIA
COLIBRI 1.05882353 1.10541645 QF_FP
Par4 1.05603164 2.69716918 AUFLIRA
Par4 1.04061625 1.28553344 BV
Alt-Ergo 1.03363914 1.0626182 UFDT
Yices 2.6.2 1.02189781 6.25725454 QF_ALIA
Yices 2.6.2 1.01813472 1.09781416 QF_LRA
Par4 1.01711491 1.03077499 QF_IDL
Yices 2.6.2 1.01006711 7.91706658 QF_UFLIA
Par4 1.00861538 1.41329805 QF_BV
Yices 2.6.2 1.00515464 1.29920072 QF_UFBV
Par4 1.00400802 1.6448974 QF_BVFP
Par4 1.00214448 1.72547434 QF_ABV
Yices 2.6.2 1.00185529 2.00261369 QF_UFLRA
Yices 2.6.2 1.0015361 19.63042443 QF_AUFLIA
Par4 1.0002849 1.06016133 QF_UF
Yices 2.6.2 1.0 12.42317995 QF_AX
Vampire 1.0 5.30200722 UFDTNIA
CVC4 1.0 5.1292046 ALIA
Alt-Ergo 1.0 1.15408998 UFLRA
MathSAT-na-ext 1.0 1.14061286 QF_ANIA
Yices 2.6.2 1.0 1.0468397 QF_LIRA
MathSAT-default 1.0 1.0322563 QF_AUFNIA

n Non-competing.