The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_NRA division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 2230 Time Limit: 2400 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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2007 | 596149.956 | 555677.176 | 2007 | 943 | 1064 | 223 | 171 | 52 |
| Yices2-fixedn | 0 | 1770 | 579354.617 | 580095.886 | 1770 | 816 | 954 | 460 | 460 | 0 |
| Yices2 | 0 | 1770 | 580325.741 | 580320.257 | 1770 | 816 | 954 | 460 | 460 | 0 |
| z3n | 0 | 1658 | 708543.567 | 708571.815 | 1658 | 830 | 828 | 572 | 566 | 0 |
| SMT-RAT-MCSAT | 0 | 1564 | 818376.861 | 818388.918 | 1564 | 751 | 813 | 666 | 632 | 8 |
| veriT+raSAT+Redlog | 0 | 1420 | 981843.147 | 975683.864 | 1420 | 635 | 785 | 810 | 808 | 0 |
| SMT-RAT-CAlC | 0 | 1377 | 1054108.107 | 1054201.898 | 1377 | 652 | 725 | 853 | 845 | 7 |
| CVC4 | 0 | 1326 | 1171389.869 | 1179135.926 | 1326 | 385 | 941 | 904 | 904 | 0 |
| MathSAT5n | 0 | 1292 | 1155964.821 | 1156083.672 | 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 | 2010 | 797634.766 | 349854.718 | 2010 | 946 | 1064 | 220 | 168 | 52 |
| Yices2-fixedn | 0 | 1770 | 579354.617 | 580095.886 | 1770 | 816 | 954 | 460 | 460 | 0 |
| Yices2 | 0 | 1770 | 580325.741 | 580320.257 | 1770 | 816 | 954 | 460 | 460 | 0 |
| z3n | 0 | 1658 | 708543.567 | 708571.815 | 1658 | 830 | 828 | 572 | 566 | 0 |
| SMT-RAT-MCSAT | 0 | 1564 | 818376.861 | 818388.918 | 1564 | 751 | 813 | 666 | 632 | 8 |
| veriT+raSAT+Redlog | 0 | 1420 | 981843.147 | 975683.864 | 1420 | 635 | 785 | 810 | 808 | 0 |
| SMT-RAT-CAlC | 0 | 1377 | 1054108.107 | 1054201.898 | 1377 | 652 | 725 | 853 | 845 | 7 |
| CVC4 | 0 | 1326 | 1171389.869 | 1179135.926 | 1326 | 385 | 941 | 904 | 904 | 0 |
| MathSAT5n | 0 | 1292 | 1155964.821 | 1156083.672 | 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 | 258651.84 | 160046.075 | 946 | 946 | 0 | 1284 | 168 | 52 |
| z3n | 0 | 830 | 237725.204 | 237708.136 | 830 | 830 | 0 | 1400 | 566 | 0 |
| Yices2 | 0 | 816 | 254720.147 | 254716.006 | 816 | 816 | 0 | 1414 | 460 | 0 |
| Yices2-fixedn | 0 | 816 | 254452.248 | 254757.121 | 816 | 816 | 0 | 1414 | 460 | 0 |
| SMT-RAT-MCSAT | 0 | 751 | 316570.746 | 316589.126 | 751 | 751 | 0 | 1479 | 632 | 8 |
| SMT-RAT-CAlC | 0 | 652 | 444998.094 | 445029.221 | 652 | 652 | 0 | 1578 | 845 | 7 |
| veriT+raSAT+Redlog | 0 | 635 | 468237.818 | 465072.718 | 635 | 635 | 0 | 1595 | 808 | 0 |
| CVC4 | 0 | 385 | 819869.182 | 826865.44 | 385 | 385 | 0 | 1845 | 904 | 0 |
| MathSAT5n | 0 | 361 | 800620.321 | 800728.362 | 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 | 75867.056 | 25397.843 | 1064 | 0 | 1064 | 1166 | 168 | 52 |
| Yices2-fixedn | 0 | 954 | 168088.824 | 168132.265 | 954 | 0 | 954 | 1276 | 460 | 0 |
| Yices2 | 0 | 954 | 168420.234 | 168398.151 | 954 | 0 | 954 | 1276 | 460 | 0 |
| CVC4 | 0 | 941 | 195650.108 | 195064.237 | 941 | 0 | 941 | 1289 | 904 | 0 |
| MathSAT5n | 0 | 931 | 198172.84 | 198148.97 | 931 | 0 | 931 | 1299 | 938 | 0 |
| z3n | 0 | 828 | 316010.776 | 316036.85 | 828 | 0 | 828 | 1402 | 566 | 0 |
| SMT-RAT-MCSAT | 0 | 813 | 338846.122 | 338824.264 | 813 | 0 | 813 | 1417 | 632 | 8 |
| veriT+raSAT+Redlog | 0 | 785 | 357119.52 | 354515.272 | 785 | 0 | 785 | 1445 | 808 | 0 |
| SMT-RAT-CAlC | 0 | 725 | 445919.453 | 445966.767 | 725 | 0 | 725 | 1505 | 845 | 7 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | 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.