The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the Equality (UF, UFDT) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 3514 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 1383 | 2777412.154 | 2799654.913 | 1383 | 439 | 944 | 2131 | 2131 | 0 |
| 2019-CVC4n | 0 | 1346 | 2965657.764 | 3011054.108 | 1346 | 407 | 939 | 2168 | 2168 | 0 |
| Vampire | 0 | 1287 | 5474528.562 | 5378651.194 | 1287 | 395 | 892 | 2227 | 2227 | 0 |
| 2018-Vampiren | 0 | 910 | 3502749.128 | 3361924.119 | 910 | 379 | 531 | 1381 | 1381 | 0 |
| Alt-Ergo | 0 | 809 | 6222627.542 | 6171171.002 | 809 | 0 | 809 | 2705 | 2514 | 56 |
| veriT | 0 | 588 | 2110950.82 | 2107671.178 | 588 | 0 | 588 | 1703 | 1677 | 25 |
| veriT+viten | 0 | 548 | 2368678.931 | 2368829.075 | 548 | 0 | 548 | 1743 | 1496 | 235 |
| z3n | 0 | 413 | 1774960.133 | 1775296.552 | 413 | 63 | 350 | 1878 | 1108 | 40 |
| SMTInterpol-fixedn | 0 | 105 | 3268435.896 | 3127574.928 | 105 | 25 | 80 | 2186 | 2166 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 12273.362 | 8321.245 | 0 | 0 | 0 | 3514 | 0 | 0 |
| SMTInterpol | 1 | 104 | 3268353.726 | 3128275.397 | 104 | 25 | 79 | 2187 | 2166 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 1383 | 2777412.154 | 2799654.913 | 1383 | 439 | 944 | 2131 | 2131 | 0 |
| 2019-CVC4n | 0 | 1346 | 2965657.764 | 3011054.108 | 1346 | 407 | 939 | 2168 | 2168 | 0 |
| Vampire | 0 | 1335 | 10487711.072 | 2693381.791 | 1335 | 413 | 922 | 2179 | 2179 | 0 |
| 2018-Vampiren | 0 | 963 | 6689597.168 | 1683175.458 | 963 | 380 | 583 | 1328 | 1328 | 0 |
| Alt-Ergo | 0 | 827 | 12069232.512 | 3160462.276 | 827 | 0 | 827 | 2687 | 2496 | 56 |
| veriT | 0 | 588 | 2110950.82 | 2107671.178 | 588 | 0 | 588 | 1703 | 1677 | 25 |
| veriT+viten | 0 | 548 | 2368678.931 | 2368829.075 | 548 | 0 | 548 | 1743 | 1496 | 235 |
| z3n | 0 | 413 | 1774960.133 | 1775296.552 | 413 | 63 | 350 | 1878 | 1108 | 40 |
| SMTInterpol-fixedn | 0 | 105 | 3938029.636 | 2604402.732 | 105 | 25 | 80 | 2186 | 2151 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 12273.362 | 8321.245 | 0 | 0 | 0 | 3514 | 0 | 0 |
| SMTInterpol | 1 | 104 | 3939787.576 | 2604171.402 | 104 | 25 | 79 | 2187 | 2152 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 439 | 282907.093 | 289035.186 | 439 | 439 | 0 | 3075 | 2131 | 0 |
| Vampire | 0 | 413 | 552486.074 | 141492.606 | 413 | 413 | 0 | 3101 | 2179 | 0 |
| 2019-CVC4n | 0 | 407 | 471131.077 | 481519.529 | 407 | 407 | 0 | 3107 | 2168 | 0 |
| 2018-Vampiren | 0 | 380 | 154281.237 | 38903.34 | 380 | 380 | 0 | 1911 | 1328 | 0 |
| z3n | 0 | 63 | 318094.207 | 318148.682 | 63 | 63 | 0 | 2228 | 1108 | 40 |
| SMTInterpol | 0 | 25 | 728775.702 | 445672.228 | 25 | 25 | 0 | 2266 | 2152 | 0 |
| SMTInterpol-fixedn | 0 | 25 | 727340.702 | 445718.386 | 25 | 25 | 0 | 2266 | 2151 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 1775.967 | 1224.225 | 0 | 0 | 0 | 3514 | 0 | 0 |
| veriT | 0 | 0 | 491515.23 | 490820.33 | 0 | 0 | 0 | 2291 | 1677 | 25 |
| Alt-Ergo | 0 | 0 | 1861646.796 | 524790.346 | 0 | 0 | 0 | 3514 | 2496 | 56 |
| veriT+viten | 0 | 0 | 643174.77 | 643213.74 | 0 | 0 | 0 | 2291 | 1496 | 235 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 944 | 152719.411 | 153727.506 | 944 | 0 | 944 | 2570 | 2131 | 0 |
| 2019-CVC4n | 0 | 939 | 170309.877 | 172621.059 | 939 | 0 | 939 | 2575 | 2168 | 0 |
| Vampire | 0 | 922 | 756160.598 | 195004.815 | 922 | 0 | 922 | 2592 | 2179 | 0 |
| Alt-Ergo | 0 | 827 | 1097848.722 | 284189.711 | 827 | 0 | 827 | 2687 | 2496 | 56 |
| veriT | 0 | 588 | 146394.74 | 146168.31 | 588 | 0 | 588 | 1703 | 1677 | 25 |
| 2018-Vampiren | 0 | 583 | 807516.461 | 203373.648 | 583 | 0 | 583 | 1708 | 1328 | 0 |
| veriT+viten | 0 | 548 | 173487.648 | 173477.795 | 548 | 0 | 548 | 1743 | 1496 | 235 |
| z3n | 0 | 350 | 321298.61 | 321356.419 | 350 | 0 | 350 | 1941 | 1108 | 40 |
| SMTInterpol-fixedn | 0 | 80 | 1015145.984 | 720451.338 | 80 | 0 | 80 | 2211 | 2151 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 3643.192 | 2448.366 | 0 | 0 | 0 | 3514 | 0 | 0 |
| SMTInterpol | 1 | 79 | 1016415.424 | 720648.567 | 79 | 0 | 79 | 2212 | 2152 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 1028 | 68138.155 | 61926.671 | 1028 | 323 | 705 | 2486 | 2486 | 0 |
| 2019-CVC4n | 0 | 774 | 66375.285 | 66351.619 | 774 | 32 | 742 | 2740 | 2740 | 0 |
| CVC4 | 0 | 770 | 66465.463 | 66462.774 | 770 | 32 | 738 | 2744 | 2744 | 0 |
| Alt-Ergo | 0 | 731 | 68982.021 | 65310.557 | 731 | 0 | 731 | 2783 | 2607 | 56 |
| 2018-Vampiren | 0 | 708 | 42853.115 | 39306.871 | 708 | 338 | 370 | 1583 | 1583 | 0 |
| veriT+viten | 0 | 534 | 43041.1 | 43025.434 | 534 | 0 | 534 | 1757 | 1521 | 235 |
| veriT | 0 | 467 | 44252.743 | 44252.679 | 467 | 0 | 467 | 1824 | 1799 | 25 |
| z3n | 0 | 380 | 46234.752 | 46226.228 | 380 | 59 | 321 | 1911 | 1871 | 40 |
| SMTInterpol-fixedn | 0 | 99 | 52664.167 | 52501.651 | 99 | 25 | 74 | 2192 | 2182 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 12294.081 | 8317.503 | 0 | 0 | 0 | 3514 | 1 | 0 |
| SMTInterpol | 1 | 98 | 52674.453 | 52501.126 | 98 | 25 | 73 | 2193 | 2182 | 0 |
n Non-competing.