The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the Equality+LinearArith (ALIA, AUFLIA, UFLIA, UFIDL, AUFLIRA, UFLRA, UFDTLIA, UFDTLIRA, AUFDTLIA, AUFDTLIRA) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 14578 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | Vampire | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 11836 | 1796092.629 | 1818138.399 | 11836 | 272 | 11564 | 2742 | 1399 | 0 |
| Alt-Ergo | 0 | 11079 | 5554715.295 | 5392275.706 | 11079 | 0 | 11079 | 3479 | 2198 | 58 |
| z3n | 0 | 3359 | 1649012.256 | 1653341.452 | 3359 | 132 | 3227 | 1621 | 1138 | 20 |
| veriT | 0 | 3317 | 1981798.447 | 1978194.825 | 3317 | 0 | 3317 | 1663 | 1491 | 13 |
| veriT+viten | 0 | 3243 | 1992282.141 | 1992331.448 | 3243 | 0 | 3243 | 1737 | 1468 | 87 |
| 2019-Par4n | 0 | 2635 | 2459071.425 | 2353217.507 | 2635 | 51 | 2584 | 1009 | 965 | 44 |
| SMTInterpol-fixedn | 0 | 2110 | 3876079.947 | 3616738.478 | 2110 | 57 | 2053 | 2870 | 2702 | 0 |
| SMTInterpol | 0 | 2109 | 3873837.766 | 3609809.483 | 2109 | 57 | 2052 | 2871 | 2700 | 0 |
| 2018-CVC4n | 0 | 1245 | 280468.12 | 285839.929 | 1245 | 204 | 1041 | 212 | 199 | 0 |
| 2019-CVC4n | 0 | 196 | 199129.654 | 205137.739 | 196 | 0 | 196 | 81 | 81 | 0 |
| 2018-Z3n | 0 | 24 | 3368.318 | 3368.9 | 24 | 4 | 20 | 2 | 2 | 0 |
| UltimateEliminator+MathSAT | 0 | 15 | 285077.488 | 247281.889 | 15 | 6 | 9 | 14563 | 120 | 0 |
| Vampire | 29 | 11890 | 7348237.895 | 6665349.589 | 11890 | 91 | 11799 | 2688 | 2659 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 11836 | 1796092.629 | 1818138.399 | 11836 | 272 | 11564 | 2742 | 1399 | 0 |
| Alt-Ergo | 0 | 11101 | 10359592.815 | 2830642.918 | 11101 | 0 | 11101 | 3457 | 2175 | 58 |
| z3n | 0 | 3359 | 1649012.256 | 1653341.452 | 3359 | 132 | 3227 | 1621 | 1138 | 20 |
| veriT | 0 | 3317 | 1981798.447 | 1978194.825 | 3317 | 0 | 3317 | 1663 | 1491 | 13 |
| veriT+viten | 0 | 3243 | 1992282.141 | 1992331.448 | 3243 | 0 | 3243 | 1737 | 1468 | 87 |
| 2019-Par4n | 0 | 2637 | 3510328.615 | 1276601.494 | 2637 | 51 | 2586 | 1007 | 963 | 44 |
| SMTInterpol-fixedn | 0 | 2110 | 4316626.717 | 3276903.527 | 2110 | 57 | 2053 | 2870 | 2695 | 0 |
| SMTInterpol | 0 | 2109 | 4312104.706 | 3276348.952 | 2109 | 57 | 2052 | 2871 | 2693 | 0 |
| 2018-CVC4n | 0 | 1245 | 280468.12 | 285839.929 | 1245 | 204 | 1041 | 212 | 199 | 0 |
| 2019-CVC4n | 0 | 196 | 199129.654 | 205137.739 | 196 | 0 | 196 | 81 | 81 | 0 |
| 2018-Z3n | 0 | 24 | 3368.318 | 3368.9 | 24 | 4 | 20 | 2 | 2 | 0 |
| UltimateEliminator+MathSAT | 0 | 15 | 365343.588 | 180085.169 | 15 | 6 | 9 | 14563 | 120 | 0 |
| Vampire | 33 | 11959 | 13408312.445 | 3450618.983 | 11959 | 91 | 11868 | 2619 | 2599 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 272 | 108508.227 | 109231.538 | 272 | 272 | 0 | 14306 | 1399 | 0 |
| 2018-CVC4n | 0 | 204 | 50144.957 | 50454.126 | 204 | 204 | 0 | 1253 | 199 | 0 |
| z3n | 0 | 132 | 62650.966 | 62661.414 | 132 | 132 | 0 | 4848 | 1138 | 20 |
| SMTInterpol-fixedn | 0 | 57 | 98491.941 | 82274.087 | 57 | 57 | 0 | 4923 | 2695 | 0 |
| SMTInterpol | 0 | 57 | 101702.624 | 83124.124 | 57 | 57 | 0 | 4923 | 2693 | 0 |
| 2019-Par4n | 0 | 51 | 10046.319 | 3968.783 | 51 | 51 | 0 | 3593 | 963 | 44 |
| UltimateEliminator+MathSAT | 0 | 6 | 1255.314 | 843.363 | 6 | 6 | 0 | 14572 | 120 | 0 |
| 2018-Z3n | 0 | 4 | 3367.118 | 3367.7 | 4 | 4 | 0 | 22 | 2 | 0 |
| 2019-CVC4n | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 277 | 81 | 0 |
| veriT+viten | 0 | 0 | 142382.823 | 142376.998 | 0 | 0 | 0 | 4980 | 1468 | 87 |
| veriT | 0 | 0 | 159849.571 | 159789.937 | 0 | 0 | 0 | 4980 | 1491 | 13 |
| Alt-Ergo | 0 | 0 | 604306.16 | 169742.313 | 0 | 0 | 0 | 14558 | 2175 | 58 |
| Vampire | 33 | 91 | 1101861.985 | 284185.871 | 91 | 91 | 0 | 14487 | 2599 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 11868 | 3347151.58 | 891211.532 | 11868 | 0 | 11868 | 2710 | 2599 | 0 |
| CVC4 | 0 | 11564 | 303286.228 | 307387.907 | 11564 | 0 | 11564 | 3014 | 1399 | 0 |
| Alt-Ergo | 0 | 11101 | 3998715.172 | 1071110.807 | 11101 | 0 | 11101 | 3457 | 2175 | 58 |
| veriT | 0 | 3317 | 532458.511 | 531286.197 | 3317 | 0 | 3317 | 1663 | 1491 | 13 |
| veriT+viten | 0 | 3243 | 601184.072 | 601162.306 | 3243 | 0 | 3243 | 1737 | 1468 | 87 |
| z3n | 0 | 3227 | 510387.47 | 512671.17 | 3227 | 0 | 3227 | 1753 | 1138 | 20 |
| 2019-Par4n | 0 | 2586 | 258399.337 | 95354.64 | 2586 | 0 | 2586 | 1058 | 963 | 44 |
| SMTInterpol-fixedn | 0 | 2053 | 2556049.509 | 1981452.469 | 2053 | 0 | 2053 | 2927 | 2695 | 0 |
| SMTInterpol | 0 | 2052 | 2548473.006 | 1980138.92 | 2052 | 0 | 2052 | 2928 | 2693 | 0 |
| 2018-CVC4n | 0 | 1041 | 59511.795 | 60926.71 | 1041 | 0 | 1041 | 416 | 199 | 0 |
| 2019-CVC4n | 0 | 196 | 113063.144 | 115131.229 | 196 | 0 | 196 | 81 | 81 | 0 |
| 2018-Z3n | 0 | 20 | 1.199 | 1.201 | 20 | 0 | 20 | 6 | 2 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 292796.858 | 143247.481 | 9 | 0 | 9 | 14569 | 120 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 11304 | 49156.212 | 49097.26 | 11304 | 180 | 11124 | 3274 | 1947 | 0 |
| Alt-Ergo | 0 | 10856 | 79406.751 | 66937.148 | 10856 | 0 | 10856 | 3702 | 2504 | 58 |
| z3n | 0 | 3294 | 41717.732 | 41696.432 | 3294 | 129 | 3165 | 1686 | 1652 | 20 |
| veriT+viten | 0 | 3215 | 42136.981 | 42084.132 | 3215 | 0 | 3215 | 1765 | 1529 | 87 |
| veriT | 0 | 2914 | 50284.249 | 50280.19 | 2914 | 0 | 2914 | 2066 | 2053 | 13 |
| 2019-Par4n | 0 | 2567 | 27868.208 | 26721.292 | 2567 | 48 | 2519 | 1077 | 1033 | 44 |
| SMTInterpol | 0 | 2041 | 72191.479 | 69399.889 | 2041 | 57 | 1984 | 2939 | 2794 | 0 |
| SMTInterpol-fixedn | 0 | 2041 | 72182.414 | 69414.057 | 2041 | 57 | 1984 | 2939 | 2794 | 0 |
| 2018-CVC4n | 0 | 1076 | 9307.671 | 9307.332 | 1076 | 111 | 965 | 381 | 379 | 0 |
| 2019-CVC4n | 0 | 27 | 6050.903 | 6050.897 | 27 | 0 | 27 | 250 | 250 | 0 |
| 2018-Z3n | 0 | 23 | 96.444 | 96.445 | 23 | 3 | 20 | 3 | 3 | 0 |
| UltimateEliminator+MathSAT | 0 | 15 | 52938.48 | 36989.102 | 15 | 6 | 9 | 14563 | 139 | 0 |
| Vampire | 28 | 9687 | 151766.265 | 132922.974 | 9687 | 81 | 9606 | 4891 | 4863 | 0 |
n Non-competing.