The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_NRA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 2841 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2597 | 677556.997 | 616433.775 | 2597 | 1212 | 1385 | 244 | 187 | 57 | |
| Yices 2.6.2 | 0 | 2164 | 1681986.24 | 1682107.466 | 2164 | 1065 | 1099 | 677 | 677 | 0 | |
| Z3n | 0 | 2081 | 1834876.671 | 1835365.162 | 2081 | 1066 | 1015 | 760 | 602 | 156 | |
| 2018-Z3n | 0 | 2075 | 1850123.97 | 1850733.561 | 2075 | 1063 | 1012 | 766 | 608 | 156 | |
| SMTRAT-MCSAT | 0 | 1973 | 2144115.154 | 2144263.156 | 1973 | 963 | 1010 | 868 | 864 | 4 | |
| veriT+raSAT+Redlog | 0 | 1869 | 2354843.112 | 2354276.769 | 1869 | 854 | 1015 | 972 | 972 | 0 | |
| CVC4 | 0 | 1778 | 2751336.709 | 2769255.463 | 1778 | 537 | 1241 | 1063 | 1063 | 0 | |
| CVC4-SymBreakn | 0 | 1708 | 2820827.97 | 2827304.725 | 1708 | 475 | 1233 | 1133 | 1133 | 0 | |
| MathSAT-default | 0 | 1698 | 2800090.263 | 2800342.765 | 1698 | 491 | 1207 | 1143 | 1142 | 1 | |
| SMT-RAT | 0 | 1696 | 2793536.872 | 2793759.463 | 1696 | 838 | 858 | 1145 | 1129 | 10 | |
| MathSAT-na-ext | 0 | 1653 | 2910508.221 | 2910679.787 | 1653 | 448 | 1205 | 1188 | 1188 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2613 | 705823.387 | 600324.226 | 2613 | 1224 | 1389 | 228 | 171 | 57 | |
| Yices 2.6.2 | 0 | 2164 | 1682098.73 | 1682083.516 | 2164 | 1065 | 1099 | 677 | 677 | 0 | |
| Z3n | 0 | 2081 | 1835040.241 | 1835339.402 | 2081 | 1066 | 1015 | 760 | 602 | 156 | |
| 2018-Z3n | 0 | 2075 | 1850291.31 | 1850706.701 | 2075 | 1063 | 1012 | 766 | 608 | 156 | |
| SMTRAT-MCSAT | 0 | 1973 | 2144232.594 | 2144232.446 | 1973 | 963 | 1010 | 868 | 864 | 4 | |
| veriT+raSAT+Redlog | 0 | 1870 | 2355012.932 | 2354111.079 | 1870 | 855 | 1015 | 971 | 971 | 0 | |
| CVC4 | 0 | 1778 | 2768511.569 | 2769210.003 | 1778 | 537 | 1241 | 1063 | 1063 | 0 | |
| CVC4-SymBreakn | 0 | 1708 | 2826404.78 | 2827259.555 | 1708 | 475 | 1233 | 1133 | 1133 | 0 | |
| MathSAT-default | 0 | 1698 | 2800292.283 | 2800297.675 | 1698 | 491 | 1207 | 1143 | 1142 | 1 | |
| SMT-RAT | 0 | 1696 | 2793766.172 | 2793715.853 | 1696 | 838 | 858 | 1145 | 1129 | 10 | |
| MathSAT-na-ext | 0 | 1653 | 2910730.171 | 2910633.867 | 1653 | 448 | 1205 | 1188 | 1188 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1224 | 316878.4 | 248173.196 | 1224 | 1224 | 0 | 1617 | 171 | 57 |
| Z3n | 0 | 1066 | 601549.548 | 601536.065 | 1066 | 1066 | 0 | 1775 | 602 | 156 |
| Yices 2.6.2 | 0 | 1065 | 620317.022 | 620319.538 | 1065 | 1065 | 0 | 1776 | 677 | 0 |
| 2018-Z3n | 0 | 1063 | 609783.414 | 609784.996 | 1063 | 1063 | 0 | 1778 | 608 | 156 |
| SMTRAT-MCSAT | 0 | 963 | 852331.327 | 852332.225 | 963 | 963 | 0 | 1878 | 864 | 4 |
| veriT+raSAT+Redlog | 0 | 855 | 1113565.504 | 1113004.534 | 855 | 855 | 0 | 1986 | 971 | 0 |
| SMT-RAT | 0 | 838 | 1147028.617 | 1147039.248 | 838 | 838 | 0 | 2003 | 1129 | 10 |
| CVC4 | 0 | 537 | 2022571.417 | 2023229.008 | 537 | 537 | 0 | 2304 | 1063 | 0 |
| MathSAT-default | 0 | 491 | 1990114.267 | 1990116.461 | 491 | 491 | 0 | 2350 | 1142 | 1 |
| CVC4-SymBreakn | 0 | 475 | 2062791.973 | 2063257.826 | 475 | 475 | 0 | 2366 | 1133 | 0 |
| MathSAT-na-ext | 0 | 448 | 2096615.506 | 2096619.695 | 448 | 448 | 0 | 2393 | 1188 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 1389 | 93744.986 | 56951.03 | 1389 | 0 | 1389 | 1452 | 171 | 57 |
| CVC4 | 0 | 1241 | 450740.151 | 450780.995 | 1241 | 0 | 1241 | 1600 | 1063 | 0 |
| CVC4-SymBreakn | 0 | 1233 | 468412.807 | 468801.729 | 1233 | 0 | 1233 | 1608 | 1133 | 0 |
| MathSAT-default | 0 | 1207 | 514978.016 | 514981.214 | 1207 | 0 | 1207 | 1634 | 1142 | 1 |
| MathSAT-na-ext | 0 | 1205 | 518914.666 | 518814.172 | 1205 | 0 | 1205 | 1636 | 1188 | 0 |
| Yices 2.6.2 | 0 | 1099 | 766581.708 | 766563.977 | 1099 | 0 | 1099 | 1742 | 677 | 0 |
| Z3n | 0 | 1015 | 940116.622 | 940101.864 | 1015 | 0 | 1015 | 1826 | 602 | 156 |
| veriT+raSAT+Redlog | 0 | 1015 | 946247.428 | 945906.545 | 1015 | 0 | 1015 | 1826 | 971 | 0 |
| 2018-Z3n | 0 | 1012 | 947135.857 | 947136.559 | 1012 | 0 | 1012 | 1829 | 608 | 156 |
| SMTRAT-MCSAT | 0 | 1010 | 996701.267 | 996700.22 | 1010 | 0 | 1010 | 1831 | 864 | 4 |
| SMT-RAT | 0 | 858 | 1351537.555 | 1351476.604 | 858 | 0 | 858 | 1983 | 1129 | 10 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2416 | 17677.202 | 12815.527 | 2416 | 1131 | 1285 | 425 | 368 | 57 | |
| Z3n | 0 | 2049 | 21794.571 | 21764.854 | 2049 | 1039 | 1010 | 792 | 636 | 156 | |
| 2018-Z3n | 0 | 2042 | 21885.66 | 21885.941 | 2042 | 1035 | 1007 | 799 | 643 | 156 | |
| Yices 2.6.2 | 0 | 2005 | 21082.834 | 21063.656 | 2005 | 1013 | 992 | 836 | 836 | 0 | |
| veriT+raSAT+Redlog | 0 | 1817 | 25536.69 | 25520.968 | 1817 | 828 | 989 | 1024 | 1024 | 0 | |
| SMTRAT-MCSAT | 0 | 1816 | 26773.837 | 26767.603 | 1816 | 946 | 870 | 1025 | 1021 | 4 | |
| SMT-RAT | 0 | 1527 | 33215.088 | 33211.721 | 1527 | 817 | 710 | 1314 | 1304 | 10 | |
| MathSAT-default | 0 | 1507 | 35199.962 | 35198.123 | 1507 | 426 | 1081 | 1334 | 1333 | 1 | |
| MathSAT-na-ext | 0 | 1461 | 36402.042 | 36362.113 | 1461 | 390 | 1071 | 1380 | 1380 | 0 | |
| CVC4 | 0 | 1340 | 39160.557 | 39126.381 | 1340 | 280 | 1060 | 1501 | 1501 | 0 | |
| CVC4-SymBreakn | 0 | 1299 | 40075.742 | 40080.832 | 1299 | 323 | 976 | 1542 | 1542 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.