The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFLIA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:07 +0000
Benchmarks: 2848 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | SMTInterpol | cvc5 | veriT |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1641 | 1471592.797 | 1456374.101 | 1641 | 7 | 1634 | 1207 | 1163 | 44 |
| 2020-CVC4n | 0 | 1615 | 1480242.838 | 1498764.669 | 1615 | 2 | 1613 | 1233 | 1202 | 0 |
| cvc5 - fixedn | 0 | 1589 | 688247.291 | 1508521.201 | 1589 | 0 | 1589 | 1259 | 1240 | 0 |
| cvc5 | 0 | 1584 | 697022.626 | 1514824.283 | 1584 | 1 | 1583 | 1264 | 1245 | 0 |
| veriT | 0 | 1558 | 1547763.299 | 1547855.941 | 1558 | 0 | 1558 | 1290 | 1252 | 2 |
| Vampire | 0 | 1451 | 1700499.522 | 1636008.943 | 1451 | 0 | 1451 | 1397 | 1345 | 0 |
| Vampire - fixedn | 0 | 1444 | 1698205.023 | 1630941.767 | 1444 | 0 | 1444 | 1404 | 1340 | 0 |
| 2020-Vampiren | 0 | 1420 | 1702023.435 | 1639319.07 | 1420 | 0 | 1420 | 1428 | 1348 | 0 |
| 2020-z3n | 0 | 1324 | 1457518.666 | 1460896.998 | 1324 | 7 | 1317 | 1524 | 972 | 9 |
| z3n | 0 | 1255 | 1508120.616 | 1516770.377 | 1255 | 7 | 1248 | 1593 | 1000 | 15 |
| iProver | 0 | 664 | 2679735.424 | 2635017.357 | 664 | 0 | 664 | 2184 | 2138 | 45 |
| SMTInterpol | 0 | 410 | 2871312.981 | 2865163.048 | 410 | 3 | 407 | 2438 | 2362 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 23602.241 | 16869.599 | 0 | 0 | 0 | 2848 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1660 | 1482580.847 | 1444909.946 | 1660 | 9 | 1651 | 1188 | 1144 | 44 |
| 2020-CVC4n | 0 | 1615 | 1497922.268 | 1498707.379 | 1615 | 2 | 1613 | 1233 | 1211 | 0 |
| cvc5 - fixedn | 0 | 1589 | 1508258.016 | 1508454.731 | 1589 | 0 | 1589 | 1259 | 1240 | 0 |
| cvc5 | 0 | 1584 | 1514481.761 | 1514759.843 | 1584 | 1 | 1583 | 1264 | 1245 | 0 |
| veriT | 0 | 1558 | 1547913.879 | 1547786.621 | 1558 | 0 | 1558 | 1290 | 1251 | 2 |
| Vampire | 0 | 1476 | 1794963.422 | 1597977.962 | 1476 | 0 | 1476 | 1372 | 1286 | 0 |
| Vampire - fixedn | 0 | 1473 | 1809357.953 | 1593600.404 | 1473 | 0 | 1473 | 1375 | 1279 | 0 |
| 2020-Vampiren | 0 | 1450 | 1802364.775 | 1604654.492 | 1450 | 0 | 1450 | 1398 | 1289 | 0 |
| 2020-z3n | 0 | 1324 | 1458752.046 | 1460856.158 | 1324 | 7 | 1317 | 1524 | 982 | 9 |
| z3n | 0 | 1255 | 1511096.896 | 1516726.237 | 1255 | 7 | 1248 | 1593 | 1000 | 15 |
| iProver | 0 | 720 | 2757168.544 | 2604321.45 | 720 | 0 | 720 | 2128 | 2082 | 45 |
| SMTInterpol | 0 | 413 | 2951289.261 | 2851222.323 | 413 | 3 | 410 | 2435 | 2313 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 23602.241 | 16869.599 | 0 | 0 | 0 | 2848 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 9 | 3029.899 | 1028.778 | 9 | 9 | 0 | 0 | 2839 | 1144 | 44 |
| z3n | 0 | 7 | 2400.286 | 2400.288 | 7 | 7 | 0 | 2 | 2839 | 1000 | 15 |
| 2020-z3n | 0 | 7 | 2400.389 | 2400.389 | 7 | 7 | 0 | 2 | 2839 | 982 | 9 |
| SMTInterpol | 0 | 3 | 2407.842 | 2404.05 | 3 | 3 | 0 | 6 | 2839 | 2313 | 0 |
| 2020-CVC4n | 0 | 2 | 5037.514 | 5120.263 | 2 | 2 | 0 | 7 | 2839 | 1211 | 0 |
| cvc5 | 0 | 1 | 7053.414 | 7147.77 | 1 | 1 | 0 | 8 | 2839 | 1245 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 44.891 | 27.676 | 0 | 0 | 0 | 9 | 2839 | 4 | 0 |
| veriT | 0 | 0 | 7202.806 | 7202.796 | 0 | 0 | 0 | 9 | 2839 | 1251 | 2 |
| cvc5 - fixedn | 0 | 0 | 7733.247 | 7733.283 | 0 | 0 | 0 | 9 | 2839 | 1240 | 0 |
| Vampire - fixedn | 0 | 0 | 14400.13 | 10797.88 | 0 | 0 | 0 | 9 | 2839 | 1279 | 0 |
| 2020-Vampiren | 0 | 0 | 10800.0 | 10800.0 | 0 | 0 | 0 | 9 | 2839 | 1289 | 0 |
| iProver | 0 | 0 | 10800.0 | 10800.0 | 0 | 0 | 0 | 9 | 2839 | 2082 | 45 |
| Vampire | 0 | 0 | 10800.0 | 10800.0 | 0 | 0 | 0 | 9 | 2839 | 1286 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1651 | 129550.948 | 93881.169 | 1651 | 0 | 1651 | 63 | 1134 | 1144 | 44 |
| 2020-CVC4n | 0 | 1613 | 161310.292 | 161990.929 | 1613 | 0 | 1613 | 101 | 1134 | 1211 | 0 |
| cvc5 - fixedn | 0 | 1589 | 167317.249 | 167502.928 | 1589 | 0 | 1589 | 125 | 1134 | 1240 | 0 |
| cvc5 | 0 | 1583 | 174210.178 | 174376.962 | 1583 | 0 | 1583 | 131 | 1134 | 1245 | 0 |
| veriT | 0 | 1558 | 217986.413 | 217882.682 | 1558 | 0 | 1558 | 156 | 1134 | 1251 | 2 |
| Vampire | 0 | 1476 | 400906.742 | 237911.71 | 1476 | 0 | 1476 | 238 | 1134 | 1286 | 0 |
| Vampire - fixedn | 0 | 1473 | 408956.223 | 232842.154 | 1473 | 0 | 1473 | 241 | 1134 | 1279 | 0 |
| 2020-Vampiren | 0 | 1450 | 412763.495 | 243903.132 | 1450 | 0 | 1450 | 264 | 1134 | 1289 | 0 |
| 2020-z3n | 0 | 1317 | 390362.541 | 390795.865 | 1317 | 0 | 1317 | 397 | 1134 | 982 | 9 |
| z3n | 0 | 1248 | 466958.121 | 468614.025 | 1248 | 0 | 1248 | 466 | 1134 | 1000 | 15 |
| iProver | 0 | 720 | 1396368.544 | 1243521.45 | 720 | 0 | 720 | 994 | 1134 | 2082 | 45 |
| SMTInterpol | 0 | 410 | 1621147.944 | 1583693.917 | 410 | 0 | 410 | 1304 | 1134 | 2313 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15754.985 | 11644.228 | 0 | 0 | 0 | 1714 | 1134 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1573 | 32251.38 | 31316.833 | 1573 | 7 | 1566 | 1275 | 1231 | 44 |
| veriT | 0 | 1484 | 34093.317 | 34091.999 | 1484 | 0 | 1484 | 1364 | 1342 | 2 |
| cvc5 | 0 | 1466 | 34674.521 | 34646.376 | 1466 | 0 | 1466 | 1382 | 1374 | 0 |
| cvc5 - fixedn | 0 | 1466 | 34682.212 | 34658.036 | 1466 | 0 | 1466 | 1382 | 1374 | 0 |
| 2020-CVC4n | 0 | 1430 | 35768.604 | 35758.117 | 1430 | 0 | 1430 | 1418 | 1411 | 0 |
| Vampire | 0 | 1278 | 49625.092 | 40834.839 | 1278 | 0 | 1278 | 1570 | 1570 | 0 |
| Vampire - fixedn | 0 | 1263 | 49404.939 | 40861.473 | 1263 | 0 | 1263 | 1585 | 1574 | 0 |
| 2020-Vampiren | 0 | 1260 | 47085.061 | 40125.53 | 1260 | 0 | 1260 | 1588 | 1564 | 0 |
| 2020-z3n | 0 | 1243 | 39857.254 | 39855.452 | 1243 | 7 | 1236 | 1605 | 1596 | 9 |
| z3n | 0 | 1156 | 41737.112 | 41735.746 | 1156 | 7 | 1149 | 1692 | 1676 | 15 |
| iProver | 0 | 541 | 68418.294 | 58841.694 | 541 | 0 | 541 | 2307 | 2261 | 45 |
| SMTInterpol | 0 | 320 | 61780.288 | 60138.172 | 320 | 3 | 317 | 2528 | 2459 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 15705.443 | 9091.635 | 0 | 0 | 0 | 2848 | 14 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.