The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Page generated on 2020-07-04 11:49:33 +0000
| Sequential Performance | Parallel Performance |
|---|---|
| CVC4-uc | CVC4-uc |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| CVC4-uc | 244199.0 | 0.1686908 | UFDT |
| CVC4-uc | 155823.0 | 2.49714256 | AUFDTLIRA |
| CVC4-uc | 78597.0 | 1.48452665 | UFNIA |
| CVC4-uc | 61865.0 | 64.8236042 | UFDTLIRA |
| CVC4-uc | 13142.0 | 0.25086508 | AUFNIRA |
| CVC4-uc | 9721.0 | 0.8015608 | UFDTNIRA |
| CVC4-uc | 5541.0 | 1.71089994 | UFFPDTLIRA |
| CVC4-uc | 3668.0 | 29.18300987 | AUFFPDTLIRA |
| CVC4-uc | 1949.0 | 26.61823239 | AUFDTNIRA |
| CVC4-uc | 49.0 | 4.28190677 | BV |
| CVC4-uc | 22.0 | 1.48431915 | BVFPLRA |
| CVC4-uc | 7.0 | 6.24717836 | UFFPDTNIRA |
| CVC4-uc | 5.0 | 1757.0717412 | LIA |
| CVC4-uc | 3.0 | 8.56855734 | AUFBVDTLIA |
| CVC4-uc | 2.45844247 | 6.84129884 | UF |
| CVC4-uc | 1.94811801 | 1143.05077716 | UFIDL |
| CVC4-uc | 1.61902505 | 8.41766352 | UFLIA |
| CVC4-uc | 1.42871356 | 2.76076201 | AUFLIA |
| Yices2 | 1.38658296 | 264.44420344 | QF_AX |
| CVC4-uc | 1.34131289 | 0.04900574 | QF_AUFLIA |
| Bitwuzla | 1.24390244 | 2.75689916 | QF_FP |
| Yices2 | 1.18633865 | 0.0542323 | QF_AUFBV |
| CVC4-uc | 1.18558126 | 8.53487393 | AUFLIRA |
| Yices2 | 1.14223429 | 3.52933125 | QF_LIA |
| SMTInterpol | 1.13333333 | 0.16515599 | UFLRA |
| CVC4-uc | 1.05116279 | 10.26805315 | QF_ALIA |
| Bitwuzla | 1.04329159 | 1.37724708 | QF_BVFP |
| Bitwuzla | 1.03524962 | 2.54675299 | QF_ABVFP |
| Yices2 | 1.02658478 | 0.58814796 | QF_LRA |
| CVC4-uc | 1.01694915 | 0.08486871 | QF_UFLRA |
| Bitwuzla | 1.01044508 | 1.3768192 | QF_BV |
| SMTInterpol | 1.00651484 | 0.17824171 | QF_UF |
| Yices2 | 1.00143701 | 0.01322848 | QF_UFBV |
| Bitwuzla | 1.00136772 | 1.15141394 | QF_ABV |
| Yices2 | 1.0 | 6.86944415 | QF_UFLIA |
| Yices2 | 1.0 | 1.12016794 | QF_UFIDL |
| Solver | Correct Score | Time Score | Division |
|---|---|---|---|
| CVC4-uc | 244199.0 | 0.11512997 | UFDT |
| CVC4-uc | 155823.0 | 1.80658887 | AUFDTLIRA |
| CVC4-uc | 78597.0 | 1.47679218 | UFNIA |
| CVC4-uc | 61865.0 | 43.87664683 | UFDTLIRA |
| CVC4-uc | 13142.0 | 0.16895646 | AUFNIRA |
| CVC4-uc | 9721.0 | 0.55981768 | UFDTNIRA |
| CVC4-uc | 5541.0 | 1.18241409 | UFFPDTLIRA |
| CVC4-uc | 3668.0 | 21.3595459 | AUFFPDTLIRA |
| CVC4-uc | 1949.0 | 19.4618563 | AUFDTNIRA |
| CVC4-uc | 49.0 | 4.23514205 | BV |
| CVC4-uc | 22.0 | 1.12626098 | BVFPLRA |
| CVC4-uc | 7.0 | 4.62623787 | UFFPDTNIRA |
| CVC4-uc | 5.0 | 1702.21472126 | LIA |
| CVC4-uc | 3.0 | 6.09188593 | AUFBVDTLIA |
| CVC4-uc | 2.45844247 | 6.81364597 | UF |
| CVC4-uc | 1.94811801 | 1140.09989644 | UFIDL |
| CVC4-uc | 1.61902505 | 8.38476094 | UFLIA |
| CVC4-uc | 1.42871356 | 2.73482702 | AUFLIA |
| Yices2 | 1.38658296 | 223.82595836 | QF_AX |
| CVC4-uc | 1.34131289 | 0.05550392 | QF_AUFLIA |
| Bitwuzla | 1.24390244 | 2.75402191 | QF_FP |
| Yices2 | 1.18633865 | 0.05426772 | QF_AUFBV |
| CVC4-uc | 1.18558126 | 8.37055396 | AUFLIRA |
| Yices2 | 1.14223429 | 3.52887889 | QF_LIA |
| SMTInterpol | 1.13333333 | 0.24633883 | UFLRA |
| CVC4-uc | 1.05116279 | 6.22405155 | QF_ALIA |
| Bitwuzla | 1.04329159 | 1.37227573 | QF_BVFP |
| Bitwuzla | 1.03524962 | 2.56339988 | QF_ABVFP |
| Yices2 | 1.02658478 | 0.58662268 | QF_LRA |
| CVC4-uc | 1.01694915 | 0.08794362 | QF_UFLRA |
| Bitwuzla | 1.01044508 | 1.37715264 | QF_BV |
| SMTInterpol | 1.00651484 | 0.31110155 | QF_UF |
| Yices2 | 1.00143701 | 0.01343085 | QF_UFBV |
| Bitwuzla | 1.00136772 | 1.15229839 | QF_ABV |
| Yices2 | 1.0 | 4.51019024 | QF_UFLIA |
| Yices2 | 1.0 | 1.02046245 | QF_UFIDL |
n Non-competing.
e Experimental.