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 2020-07-04 11:46:59 +0000
Benchmarks: 2230 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1998 | 325585.346 | 294271.298 | 1998 | 937 | 1061 | 232 | 180 | 52 | |
| Yices2-fixedn | 0 | 1770 | 579351.637 | 580091.866 | 1770 | 816 | 954 | 460 | 460 | 0 | |
| Yices2 | 0 | 1770 | 580322.491 | 580314.797 | 1770 | 816 | 954 | 460 | 460 | 0 | |
| z3n | 0 | 1658 | 708539.767 | 708566.395 | 1658 | 830 | 828 | 572 | 566 | 0 | |
| SMT-RAT-MCSAT | 0 | 1564 | 808770.651 | 808779.078 | 1564 | 751 | 813 | 666 | 632 | 8 | |
| veriT+raSAT+Redlog | 0 | 1420 | 975715.937 | 975662.684 | 1420 | 635 | 785 | 810 | 808 | 0 | |
| SMT-RAT-CAlC | 0 | 1377 | 1045700.847 | 1045791.558 | 1377 | 652 | 725 | 853 | 845 | 7 | |
| CVC4 | 0 | 1325 | 1169585.429 | 1179419.785 | 1325 | 385 | 940 | 905 | 905 | 0 | |
| MathSAT5n | 0 | 1292 | 1155961.421 | 1156078.182 | 1292 | 361 | 931 | 938 | 938 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2010 | 333813.256 | 287439.958 | 2010 | 946 | 1064 | 220 | 168 | 52 | |
| Yices2-fixedn | 0 | 1770 | 580033.882 | 580073.896 | 1770 | 816 | 954 | 460 | 460 | 0 | |
| Yices2 | 0 | 1770 | 580374.371 | 580298.647 | 1770 | 816 | 954 | 460 | 460 | 0 | |
| z3n | 0 | 1658 | 708610.427 | 708547.195 | 1658 | 830 | 828 | 572 | 566 | 0 | |
| SMT-RAT-MCSAT | 0 | 1564 | 808820.671 | 808759.198 | 1564 | 751 | 813 | 666 | 632 | 8 | |
| veriT+raSAT+Redlog | 0 | 1420 | 975761.947 | 975644.694 | 1420 | 635 | 785 | 810 | 808 | 0 | |
| SMT-RAT-CAlC | 0 | 1377 | 1045783.947 | 1045762.018 | 1377 | 652 | 725 | 853 | 845 | 7 | |
| CVC4 | 0 | 1326 | 1179005.929 | 1179094.776 | 1326 | 385 | 941 | 904 | 904 | 0 | |
| MathSAT5n | 0 | 1292 | 1156089.651 | 1156039.582 | 1292 | 361 | 931 | 938 | 938 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 946 | 134294.83 | 104843.315 | 946 | 946 | 0 | 1284 | 168 | 52 |
| z3n | 0 | 830 | 237748.324 | 237699.536 | 830 | 830 | 0 | 1400 | 566 | 0 |
| Yices2 | 0 | 816 | 254741.897 | 254706.176 | 816 | 816 | 0 | 1414 | 460 | 0 |
| Yices2-fixedn | 0 | 816 | 254729.098 | 254746.901 | 816 | 816 | 0 | 1414 | 460 | 0 |
| SMT-RAT-MCSAT | 0 | 751 | 316588.126 | 316577.986 | 751 | 751 | 0 | 1479 | 632 | 8 |
| SMT-RAT-CAlC | 0 | 652 | 443829.654 | 443811.591 | 652 | 652 | 0 | 1578 | 845 | 7 |
| veriT+raSAT+Redlog | 0 | 635 | 465121.218 | 465053.788 | 635 | 635 | 0 | 1595 | 808 | 0 |
| CVC4 | 0 | 385 | 826466.362 | 826835.56 | 385 | 385 | 0 | 1845 | 904 | 0 |
| MathSAT5n | 0 | 361 | 800695.491 | 800697.572 | 361 | 361 | 0 | 1869 | 938 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1064 | 42318.426 | 25396.643 | 1064 | 0 | 1064 | 1166 | 168 | 52 |
| Yices2-fixedn | 0 | 954 | 168104.784 | 168126.995 | 954 | 0 | 954 | 1276 | 460 | 0 |
| Yices2 | 0 | 954 | 168432.474 | 168392.471 | 954 | 0 | 954 | 1276 | 460 | 0 |
| CVC4 | 0 | 941 | 195339.568 | 195059.217 | 941 | 0 | 941 | 1289 | 904 | 0 |
| MathSAT5n | 0 | 931 | 198194.16 | 198142.01 | 931 | 0 | 931 | 1299 | 938 | 0 |
| z3n | 0 | 828 | 316040.786 | 316026.34 | 828 | 0 | 828 | 1402 | 566 | 0 |
| SMT-RAT-MCSAT | 0 | 813 | 336463.282 | 336411.554 | 813 | 0 | 813 | 1417 | 632 | 8 |
| veriT+raSAT+Redlog | 0 | 785 | 354551.18 | 354501.652 | 785 | 0 | 785 | 1445 | 808 | 0 |
| SMT-RAT-CAlC | 0 | 725 | 444754.293 | 444750.427 | 725 | 0 | 725 | 1505 | 845 | 7 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1889 | 14257.489 | 10323.972 | 1889 | 889 | 1000 | 341 | 289 | 52 | |
| Yices2 | 0 | 1666 | 14357.316 | 14358.132 | 1666 | 779 | 887 | 564 | 564 | 0 | |
| Yices2-fixedn | 0 | 1666 | 14363.767 | 14364.913 | 1666 | 779 | 887 | 564 | 564 | 0 | |
| z3n | 0 | 1593 | 17711.919 | 17691.094 | 1593 | 802 | 791 | 637 | 632 | 0 | |
| SMT-RAT-MCSAT | 0 | 1445 | 20675.031 | 20652.75 | 1445 | 730 | 715 | 785 | 777 | 8 | |
| veriT+raSAT+Redlog | 0 | 1394 | 20733.113 | 20721.203 | 1394 | 619 | 775 | 836 | 836 | 0 | |
| SMT-RAT-CAlC | 0 | 1251 | 25197.195 | 25171.847 | 1251 | 646 | 605 | 979 | 972 | 7 | |
| MathSAT5n | 0 | 1163 | 27996.385 | 27995.378 | 1163 | 317 | 846 | 1067 | 1067 | 0 | |
| CVC4 | 0 | 1002 | 31768.353 | 31728.2 | 1002 | 197 | 805 | 1228 | 1228 | 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.