The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_NIA division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 9195 Time Limit: 1200 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 | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7009 | 2941229.205 | 2714107.019 | 7009 | 4808 | 2201 | 2186 | 2169 | 17 | |
| CVC4 | 0 | 6345 | 4536468.213 | 4566379.554 | 6345 | 4593 | 1752 | 2850 | 2850 | 0 | |
| MathSAT5n | 0 | 6330 | 3792550.67 | 3792733.7 | 6330 | 4377 | 1953 | 2865 | 2865 | 0 | |
| Yices2 | 0 | 6074 | 3893392.826 | 3893617.254 | 6074 | 4075 | 1999 | 3121 | 3121 | 0 | |
| Yices2-fixedn | 0 | 6073 | 3875730.091 | 3903442.246 | 6073 | 4074 | 1999 | 3122 | 3122 | 0 | |
| z3n | 0 | 5955 | 3862190.848 | 3862125.194 | 5955 | 4334 | 1621 | 3240 | 2646 | 6 | |
| AProVE | 0 | 3184 | 6032877.719 | 7377595.572 | 3184 | 3184 | 0 | 6011 | 5937 | 0 | |
| SMT-RAT | 0 | 1996 | 8808232.926 | 8809398.729 | 1996 | 1801 | 195 | 7199 | 7166 | 3 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 7183 | 3130972.535 | 2611375.017 | 7183 | 4952 | 2231 | 2012 | 1995 | 17 | |
| CVC4 | 0 | 6346 | 4564678.227 | 4565830.626 | 6346 | 4594 | 1752 | 2849 | 2849 | 0 | |
| MathSAT5n | 0 | 6330 | 3793231.75 | 3792607.62 | 6330 | 4377 | 1953 | 2865 | 2865 | 0 | |
| Yices2 | 0 | 6074 | 3893742.976 | 3893513.494 | 6074 | 4075 | 1999 | 3121 | 3121 | 0 | |
| Yices2-fixedn | 0 | 6073 | 3902022.371 | 3903316.016 | 6073 | 4074 | 1999 | 3122 | 3122 | 0 | |
| z3n | 0 | 5955 | 3862486.788 | 3862034.654 | 5955 | 4334 | 1621 | 3240 | 2646 | 6 | |
| AProVE | 0 | 3186 | 7388501.518 | 7377531.142 | 3186 | 3186 | 0 | 6009 | 5935 | 0 | |
| SMT-RAT | 0 | 1996 | 8809200.426 | 8809104.329 | 1996 | 1801 | 195 | 7199 | 7166 | 3 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 4952 | 1033463.156 | 640144.427 | 4952 | 4952 | 0 | 4243 | 1995 | 17 |
| CVC4 | 0 | 4594 | 1940019.392 | 1941282.29 | 4594 | 4594 | 0 | 4601 | 2849 | 0 |
| MathSAT5n | 0 | 4377 | 1460777.563 | 1460296.15 | 4377 | 4377 | 0 | 4818 | 2865 | 0 |
| z3n | 0 | 4334 | 1400034.439 | 1399717.3 | 4334 | 4334 | 0 | 4861 | 2646 | 6 |
| Yices2 | 0 | 4075 | 1655800.327 | 1655601.048 | 4075 | 4075 | 0 | 5120 | 3121 | 0 |
| Yices2-fixedn | 0 | 4074 | 1661985.021 | 1662501.461 | 4074 | 4074 | 0 | 5121 | 3122 | 0 |
| AProVE | 0 | 3186 | 2850073.499 | 2839113.429 | 3186 | 3186 | 0 | 6009 | 5935 | 0 |
| SMT-RAT | 0 | 1801 | 4459454.693 | 4459259.798 | 1801 | 1801 | 0 | 7394 | 7166 | 3 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2231 | 265108.628 | 160809.07 | 2231 | 0 | 2231 | 6964 | 1995 | 17 |
| Yices2 | 0 | 1999 | 427142.649 | 427112.447 | 1999 | 0 | 1999 | 7196 | 3121 | 0 |
| Yices2-fixedn | 0 | 1999 | 429237.351 | 430014.555 | 1999 | 0 | 1999 | 7196 | 3122 | 0 |
| MathSAT5n | 0 | 1953 | 521654.187 | 521511.47 | 1953 | 0 | 1953 | 7242 | 2865 | 0 |
| CVC4 | 0 | 1752 | 813858.835 | 813748.336 | 1752 | 0 | 1752 | 7443 | 2849 | 0 |
| z3n | 0 | 1621 | 908614.652 | 908527.482 | 1621 | 0 | 1621 | 7574 | 2646 | 6 |
| SMT-RAT | 0 | 195 | 2538945.733 | 2539044.531 | 195 | 0 | 195 | 9000 | 7166 | 3 |
| AProVE | 0 | 0 | 2790001.676 | 2790001.082 | 0 | 0 | 0 | 9195 | 5935 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 6288 | 127657.453 | 86631.865 | 6288 | 4279 | 2009 | 2907 | 2890 | 17 | |
| Yices2 | 0 | 5345 | 104190.735 | 104002.702 | 5345 | 3486 | 1859 | 3850 | 3850 | 0 | |
| Yices2-fixedn | 0 | 5337 | 104477.715 | 104357.874 | 5337 | 3480 | 1857 | 3858 | 3858 | 0 | |
| MathSAT5n | 0 | 4687 | 129075.367 | 128734.012 | 4687 | 3132 | 1555 | 4508 | 4508 | 0 | |
| z3n | 0 | 4232 | 139917.114 | 139670.715 | 4232 | 3051 | 1181 | 4963 | 4940 | 6 | |
| CVC4 | 0 | 3517 | 151428.081 | 151178.567 | 3517 | 2359 | 1158 | 5678 | 5678 | 0 | |
| AProVE | 0 | 2404 | 175808.845 | 169727.717 | 2404 | 2404 | 0 | 6791 | 6717 | 0 | |
| SMT-RAT | 0 | 1333 | 195190.621 | 195031.377 | 1333 | 1163 | 170 | 7862 | 7855 | 3 |
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.