The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_NonLinearIntArith division in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 12231 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | Z3++ | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3++-fixedn | 0 | 9982 | 3091737.894 | 3091312.854 | 9982 | 6781 | 3201 | 2247 | 2 | 2023 | 0 |
| Yices-ismt-fixedn | 0 | 9759 | 3619046.413 | 3618887.459 | 9759 | 6904 | 2855 | 2470 | 2 | 968 | 1 |
| 2019-Par4n | 0 | 9348 | 3858525.23 | 3576949.234 | 9348 | 6298 | 3050 | 2881 | 2 | 2847 | 34 |
| z3-4.8.17n | 0 | 9247 | 4149050.887 | 4148646.925 | 9247 | 6311 | 2936 | 2984 | 0 | 2978 | 0 |
| MathSATn | 0 | 8322 | 5121725.169 | 5121609.734 | 8322 | 5573 | 2749 | 3909 | 0 | 3910 | 0 |
| cvc5 | 0 | 8302 | 6487122.646 | 6542536.51 | 8302 | 5786 | 2516 | 3929 | 0 | 3924 | 5 |
| Yices2 | 0 | 7862 | 5445586.23 | 5445943.186 | 7862 | 5100 | 2762 | 4369 | 0 | 4367 | 0 |
| Z3++ | 1 | 10158 | 3077399.006 | 3076590.489 | 10158 | 6955 | 3203 | 2071 | 2 | 2013 | 0 |
| Yices-ismt | 26 | 9817 | 3493483.962 | 3493344.451 | 9817 | 6966 | 2851 | 2412 | 2 | 1940 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3++-fixedn | 0 | 9982 | 3091874.434 | 3091240.024 | 9982 | 6781 | 3201 | 2247 | 2 | 2023 | 0 |
| Yices-ismt-fixedn | 0 | 9759 | 3619713.013 | 3618838.619 | 9759 | 6904 | 2855 | 2470 | 2 | 998 | 1 |
| 2019-Par4n | 0 | 9567 | 4083392.35 | 3444119.982 | 9567 | 6488 | 3079 | 2662 | 2 | 2628 | 34 |
| z3-4.8.17n | 0 | 9247 | 4149427.317 | 4148527.045 | 9247 | 6311 | 2936 | 2984 | 0 | 2978 | 0 |
| MathSATn | 0 | 8321 | 5122487.599 | 5121439.054 | 8321 | 5572 | 2749 | 3910 | 0 | 3910 | 0 |
| cvc5 | 0 | 8303 | 6536641.848 | 6541929.025 | 8303 | 5787 | 2516 | 3928 | 0 | 3923 | 5 |
| Yices2 | 0 | 7862 | 5446154.84 | 5445786.346 | 7862 | 5100 | 2762 | 4369 | 0 | 4367 | 0 |
| Z3++ | 1 | 10158 | 3077521.356 | 3076521.269 | 10158 | 6955 | 3203 | 2071 | 2 | 2013 | 0 |
| Yices-ismt | 26 | 9817 | 3493752.752 | 3493131.591 | 9817 | 6966 | 2851 | 2412 | 2 | 1980 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices-ismt-fixedn | 0 | 6904 | 868968.315 | 868585.701 | 6904 | 6904 | 0 | 339 | 4988 | 998 | 1 |
| Z3++-fixedn | 0 | 6781 | 936525.524 | 936024.343 | 6781 | 6781 | 0 | 462 | 4988 | 2023 | 0 |
| 2019-Par4n | 0 | 6488 | 1607830.875 | 1103768.178 | 6488 | 6488 | 0 | 755 | 4988 | 2628 | 34 |
| z3-4.8.17n | 0 | 6311 | 1511226.246 | 1510555.559 | 6311 | 6311 | 0 | 932 | 4988 | 2978 | 0 |
| cvc5 | 0 | 5787 | 3470314.559 | 3475681.333 | 5787 | 5787 | 0 | 1456 | 4988 | 3923 | 5 |
| MathSATn | 0 | 5572 | 2344987.845 | 2344263.769 | 5572 | 5572 | 0 | 1671 | 4988 | 3910 | 0 |
| Yices2 | 0 | 5100 | 2723709.655 | 2723411.298 | 5100 | 5100 | 0 | 2143 | 4988 | 4367 | 0 |
| Z3++ | 1 | 6955 | 925715.127 | 925099.504 | 6955 | 6955 | 0 | 288 | 4988 | 2013 | 0 |
| Yices-ismt | 26 | 6966 | 776779.311 | 776293.413 | 6966 | 6966 | 0 | 277 | 4988 | 1980 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3++ | 0 | 3203 | 428617.763 | 428231.158 | 3203 | 0 | 3203 | 330 | 8698 | 2013 | 0 |
| Z3++-fixedn | 0 | 3201 | 431179.084 | 431045.379 | 3201 | 0 | 3201 | 332 | 8698 | 2023 | 0 |
| 2019-Par4n | 0 | 3079 | 724761.244 | 596837.574 | 3079 | 0 | 3079 | 454 | 8698 | 2628 | 34 |
| z3-4.8.17n | 0 | 2936 | 893401.071 | 893171.485 | 2936 | 0 | 2936 | 598 | 8697 | 2978 | 0 |
| Yices-ismt-fixedn | 0 | 2855 | 1007521.638 | 1007157.359 | 2855 | 0 | 2855 | 678 | 8698 | 998 | 1 |
| Yices-ismt | 0 | 2851 | 973500.001 | 973334.788 | 2851 | 0 | 2851 | 682 | 8698 | 1980 | 1 |
| Yices2 | 0 | 2762 | 977645.186 | 977575.048 | 2762 | 0 | 2762 | 772 | 8697 | 4367 | 0 |
| MathSATn | 0 | 2749 | 1032699.754 | 1032375.285 | 2749 | 0 | 2749 | 785 | 8697 | 3910 | 0 |
| cvc5 | 0 | 2516 | 1321527.288 | 1321447.692 | 2516 | 0 | 2516 | 1018 | 8697 | 3923 | 5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 8410 | 167165.287 | 114362.001 | 8410 | 5594 | 2816 | 3819 | 2 | 3785 | 34 |
| Yices2 | 0 | 6817 | 144922.142 | 144744.512 | 6817 | 4349 | 2468 | 5414 | 0 | 5414 | 0 |
| Yices-ismt | 0 | 6817 | 145027.615 | 144746.157 | 6817 | 4349 | 2468 | 5412 | 2 | 5411 | 1 |
| Yices-ismt-fixedn | 0 | 6815 | 144951.618 | 144754.431 | 6815 | 4347 | 2468 | 5414 | 2 | 5413 | 1 |
| Z3++-fixedn | 0 | 6569 | 157870.651 | 157583.735 | 6569 | 3840 | 2729 | 5660 | 2 | 5660 | 0 |
| Z3++ | 0 | 6569 | 157966.231 | 157612.653 | 6569 | 3843 | 2726 | 5660 | 2 | 5660 | 0 |
| z3-4.8.17n | 0 | 6518 | 164496.384 | 163983.261 | 6518 | 4429 | 2089 | 5713 | 0 | 5713 | 0 |
| MathSATn | 0 | 6340 | 169236.477 | 168881.149 | 6340 | 4049 | 2291 | 5891 | 0 | 5891 | 0 |
| cvc5 | 0 | 4252 | 210521.191 | 210297.849 | 4252 | 2194 | 2058 | 7979 | 0 | 7974 | 5 |
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.