The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Page generated on 2019-07-23 17:56:11 +0000
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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.
e Experimental.