The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_Equality (QF_UF, QF_AX, QF_DT) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 3104 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 3103 | 5976.078 | 5939.991 | 3103 | 1297 | 1806 | 1 | 1 | 0 |
| CVC4 | 0 | 3101 | 11835.786 | 11824.849 | 3101 | 1297 | 1804 | 3 | 3 | 0 |
| Yices2 | 0 | 3100 | 377.854 | 389.821 | 3100 | 1294 | 1806 | 0 | 0 | 0 |
| Yices2-fixedn | 0 | 3100 | 378.022 | 395.098 | 3100 | 1294 | 1806 | 0 | 0 | 0 |
| 2019-Yices 2.6.2n | 0 | 3100 | 380.54 | 393.404 | 3100 | 1294 | 1806 | 0 | 0 | 0 |
| SMTInterpol | 0 | 3065 | 61922.773 | 53622.605 | 3065 | 1294 | 1771 | 35 | 35 | 0 |
| SMTInterpol-fixedn | 0 | 3065 | 62137.076 | 53638.109 | 3065 | 1294 | 1771 | 35 | 35 | 0 |
| MathSAT5n | 0 | 3045 | 45305.262 | 45300.706 | 3045 | 1277 | 1768 | 55 | 34 | 0 |
| 2019-Par4n | 0 | 2800 | 496.93 | 376.245 | 2800 | 1130 | 1670 | 0 | 0 | 0 |
| veriT | 0 | 2800 | 791.191 | 790.47 | 2800 | 1130 | 1670 | 0 | 0 | 0 |
| OpenSMT | 0 | 2798 | 9544.475 | 9488.887 | 2798 | 1130 | 1668 | 2 | 2 | 0 |
| Alt-Ergo | 0 | 1423 | 1946775.926 | 1439907.61 | 1423 | 0 | 1423 | 1681 | 494 | 19 |
| 2018-Yicesn | 0 | 300 | 4.526 | 6.611 | 300 | 164 | 136 | 0 | 0 | 0 |
| 2018-CVC4n | 0 | 4 | 25.987 | 25.992 | 4 | 3 | 1 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 3103 | 5976.078 | 5939.991 | 3103 | 1297 | 1806 | 1 | 1 | 0 |
| CVC4 | 0 | 3101 | 11835.786 | 11824.849 | 3101 | 1297 | 1804 | 3 | 3 | 0 |
| Yices2 | 0 | 3100 | 377.854 | 389.821 | 3100 | 1294 | 1806 | 0 | 0 | 0 |
| 2019-Yices 2.6.2n | 0 | 3100 | 380.54 | 393.404 | 3100 | 1294 | 1806 | 0 | 0 | 0 |
| Yices2-fixedn | 0 | 3100 | 378.022 | 395.098 | 3100 | 1294 | 1806 | 0 | 0 | 0 |
| SMTInterpol | 0 | 3065 | 61922.773 | 53622.605 | 3065 | 1294 | 1771 | 35 | 35 | 0 |
| SMTInterpol-fixedn | 0 | 3065 | 62137.076 | 53638.109 | 3065 | 1294 | 1771 | 35 | 35 | 0 |
| MathSAT5n | 0 | 3045 | 45305.262 | 45300.706 | 3045 | 1277 | 1768 | 55 | 34 | 0 |
| 2019-Par4n | 0 | 2800 | 496.93 | 376.245 | 2800 | 1130 | 1670 | 0 | 0 | 0 |
| veriT | 0 | 2800 | 791.191 | 790.47 | 2800 | 1130 | 1670 | 0 | 0 | 0 |
| OpenSMT | 0 | 2798 | 9544.475 | 9488.887 | 2798 | 1130 | 1668 | 2 | 2 | 0 |
| Alt-Ergo | 0 | 1543 | 2835124.026 | 837067.46 | 1543 | 0 | 1543 | 1561 | 362 | 19 |
| 2018-Yicesn | 0 | 300 | 4.526 | 6.611 | 300 | 164 | 136 | 0 | 0 | 0 |
| 2018-CVC4n | 0 | 4 | 25.987 | 25.992 | 4 | 3 | 1 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1297 | 208.809 | 208.959 | 1297 | 1297 | 0 | 1807 | 1 | 0 |
| CVC4 | 0 | 1297 | 1015.07 | 1013.329 | 1297 | 1297 | 0 | 1807 | 3 | 0 |
| Yices2 | 0 | 1294 | 48.371 | 54.604 | 1294 | 1294 | 0 | 1806 | 0 | 0 |
| 2019-Yices 2.6.2n | 0 | 1294 | 49.994 | 56.605 | 1294 | 1294 | 0 | 1806 | 0 | 0 |
| Yices2-fixedn | 0 | 1294 | 48.39 | 57.154 | 1294 | 1294 | 0 | 1806 | 0 | 0 |
| SMTInterpol | 0 | 1294 | 2791.267 | 1154.351 | 1294 | 1294 | 0 | 1806 | 35 | 0 |
| SMTInterpol-fixedn | 0 | 1294 | 2763.5 | 1154.864 | 1294 | 1294 | 0 | 1806 | 35 | 0 |
| MathSAT5n | 0 | 1277 | 140.243 | 140.405 | 1277 | 1277 | 0 | 1823 | 34 | 0 |
| 2019-Par4n | 0 | 1130 | 21.092 | 53.343 | 1130 | 1130 | 0 | 1670 | 0 | 0 |
| veriT | 0 | 1130 | 107.604 | 106.694 | 1130 | 1130 | 0 | 1670 | 0 | 0 |
| OpenSMT | 0 | 1130 | 429.615 | 428.869 | 1130 | 1130 | 0 | 1670 | 2 | 0 |
| 2018-Yicesn | 0 | 164 | 1.364 | 2.775 | 164 | 164 | 0 | 136 | 0 | 0 |
| 2018-CVC4n | 0 | 3 | 0.045 | 0.044 | 3 | 3 | 0 | 1 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 731206.109 | 275010.311 | 0 | 0 | 0 | 3104 | 362 | 19 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1806 | 329.482 | 335.217 | 1806 | 0 | 1806 | 1294 | 0 | 0 |
| 2019-Yices 2.6.2n | 0 | 1806 | 330.545 | 336.799 | 1806 | 0 | 1806 | 1294 | 0 | 0 |
| Yices2-fixedn | 0 | 1806 | 329.632 | 337.943 | 1806 | 0 | 1806 | 1294 | 0 | 0 |
| z3n | 0 | 1806 | 5767.269 | 5731.031 | 1806 | 0 | 1806 | 1298 | 1 | 0 |
| CVC4 | 0 | 1804 | 10820.715 | 10811.52 | 1804 | 0 | 1804 | 1300 | 3 | 0 |
| SMTInterpol | 0 | 1771 | 59131.506 | 52468.254 | 1771 | 0 | 1771 | 1329 | 35 | 0 |
| SMTInterpol-fixedn | 0 | 1771 | 59373.576 | 52483.244 | 1771 | 0 | 1771 | 1329 | 35 | 0 |
| MathSAT5n | 0 | 1768 | 45165.019 | 45160.301 | 1768 | 0 | 1768 | 1332 | 34 | 0 |
| 2019-Par4n | 0 | 1670 | 475.838 | 322.902 | 1670 | 0 | 1670 | 1130 | 0 | 0 |
| veriT | 0 | 1670 | 683.587 | 683.776 | 1670 | 0 | 1670 | 1130 | 0 | 0 |
| OpenSMT | 0 | 1668 | 9114.86 | 9060.018 | 1668 | 0 | 1668 | 1132 | 2 | 0 |
| Alt-Ergo | 0 | 1543 | 2103917.917 | 562057.149 | 1543 | 0 | 1543 | 1561 | 362 | 19 |
| 2018-Yicesn | 0 | 136 | 3.162 | 3.836 | 136 | 0 | 136 | 164 | 0 | 0 |
| 2018-CVC4n | 0 | 1 | 25.942 | 25.948 | 1 | 0 | 1 | 3 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3098 | 251.639 | 263.602 | 3098 | 1294 | 1804 | 2 | 2 | 0 |
| 2019-Yices 2.6.2n | 0 | 3098 | 252.781 | 265.628 | 3098 | 1294 | 1804 | 2 | 2 | 0 |
| Yices2-fixedn | 0 | 3098 | 251.367 | 268.431 | 3098 | 1294 | 1804 | 2 | 2 | 0 |
| z3n | 0 | 3073 | 2013.144 | 2001.891 | 3073 | 1295 | 1778 | 31 | 31 | 0 |
| CVC4 | 0 | 3063 | 3086.754 | 3074.451 | 3063 | 1294 | 1769 | 41 | 41 | 0 |
| SMTInterpol | 0 | 3019 | 11736.932 | 6001.101 | 3019 | 1293 | 1726 | 81 | 81 | 0 |
| SMTInterpol-fixedn | 0 | 3019 | 11752.714 | 6004.65 | 3019 | 1293 | 1726 | 81 | 81 | 0 |
| MathSAT5n | 0 | 3015 | 2439.753 | 2428.148 | 3015 | 1277 | 1738 | 85 | 64 | 0 |
| 2019-Par4n | 0 | 2798 | 188.71 | 246.037 | 2798 | 1130 | 1668 | 2 | 2 | 0 |
| veriT | 0 | 2798 | 351.712 | 350.944 | 2798 | 1130 | 1668 | 2 | 2 | 0 |
| OpenSMT | 0 | 2766 | 2770.973 | 2760.091 | 2766 | 1127 | 1639 | 34 | 34 | 0 |
| Alt-Ergo | 0 | 863 | 76869.944 | 53676.944 | 863 | 0 | 863 | 2241 | 1847 | 19 |
| 2018-Yicesn | 0 | 300 | 4.526 | 6.611 | 300 | 164 | 136 | 0 | 0 | 0 |
| 2018-CVC4n | 0 | 3 | 24.045 | 24.044 | 3 | 3 | 0 | 1 | 1 | 0 |
n Non-competing.