The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_NIA logic in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 12229 Time Limit: 1200 seconds Memory Limit: 60 GB
| 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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3++-fixedn | 0 | 9982 | 3091737.894 | 3091312.854 | 9982 | 6781 | 3201 | 2247 | 2023 | 0 |
| Yices-ismt-fixedn | 0 | 9759 | 3619046.413 | 3618887.459 | 9759 | 6904 | 2855 | 2470 | 968 | 1 |
| 2019-Par4n | 0 | 9348 | 3858525.23 | 3576949.234 | 9348 | 6298 | 3050 | 2881 | 2847 | 34 |
| z3-4.8.17n | 0 | 9246 | 4147847.693 | 4147443.732 | 9246 | 6311 | 2935 | 2983 | 2977 | 0 |
| MathSATn | 0 | 8321 | 5120282.761 | 5120166.971 | 8321 | 5573 | 2748 | 3908 | 3909 | 0 |
| cvc5 | 0 | 8301 | 6485711.097 | 6541124.41 | 8301 | 5786 | 2515 | 3928 | 3923 | 5 |
| Yices2 | 0 | 7862 | 5443186.54 | 5443543.126 | 7862 | 5100 | 2762 | 4367 | 4365 | 0 |
| Z3++ | 1 | 10158 | 3077399.006 | 3076590.489 | 10158 | 6955 | 3203 | 2071 | 2013 | 0 |
| Yices-ismt | 26 | 9817 | 3493483.962 | 3493344.451 | 9817 | 6966 | 2851 | 2412 | 1940 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3++-fixedn | 0 | 9982 | 3091874.434 | 3091240.024 | 9982 | 6781 | 3201 | 2247 | 2023 | 0 |
| Yices-ismt-fixedn | 0 | 9759 | 3619713.013 | 3618838.619 | 9759 | 6904 | 2855 | 2470 | 998 | 1 |
| 2019-Par4n | 0 | 9567 | 4083392.35 | 3444119.982 | 9567 | 6488 | 3079 | 2662 | 2628 | 34 |
| z3-4.8.17n | 0 | 9246 | 4148224.123 | 4147323.852 | 9246 | 6311 | 2935 | 2983 | 2977 | 0 |
| MathSATn | 0 | 8320 | 5121044.971 | 5119996.311 | 8320 | 5572 | 2748 | 3909 | 3909 | 0 |
| cvc5 | 0 | 8302 | 6535229.839 | 6540516.955 | 8302 | 5787 | 2515 | 3927 | 3922 | 5 |
| Yices2 | 0 | 7862 | 5443754.84 | 5443386.346 | 7862 | 5100 | 2762 | 4367 | 4365 | 0 |
| Z3++ | 1 | 10158 | 3077521.356 | 3076521.269 | 10158 | 6955 | 3203 | 2071 | 2013 | 0 |
| Yices-ismt | 26 | 9817 | 3493752.752 | 3493131.591 | 9817 | 6966 | 2851 | 2412 | 1980 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices-ismt-fixedn | 0 | 6904 | 868968.315 | 868585.701 | 6904 | 6904 | 0 | 339 | 4986 | 998 | 1 |
| Z3++-fixedn | 0 | 6781 | 936525.524 | 936024.343 | 6781 | 6781 | 0 | 462 | 4986 | 2023 | 0 |
| 2019-Par4n | 0 | 6488 | 1607830.875 | 1103768.178 | 6488 | 6488 | 0 | 755 | 4986 | 2628 | 34 |
| z3-4.8.17n | 0 | 6311 | 1511226.246 | 1510555.559 | 6311 | 6311 | 0 | 932 | 4986 | 2977 | 0 |
| cvc5 | 0 | 5787 | 3470314.559 | 3475681.333 | 5787 | 5787 | 0 | 1456 | 4986 | 3922 | 5 |
| MathSATn | 0 | 5572 | 2344987.845 | 2344263.769 | 5572 | 5572 | 0 | 1671 | 4986 | 3909 | 0 |
| Yices2 | 0 | 5100 | 2723709.655 | 2723411.298 | 5100 | 5100 | 0 | 2143 | 4986 | 4365 | 0 |
| Z3++ | 1 | 6955 | 925715.127 | 925099.504 | 6955 | 6955 | 0 | 288 | 4986 | 2013 | 0 |
| Yices-ismt | 26 | 6966 | 776779.311 | 776293.413 | 6966 | 6966 | 0 | 277 | 4986 | 1980 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3++ | 0 | 3203 | 428617.763 | 428231.158 | 3203 | 0 | 3203 | 330 | 8696 | 2013 | 0 |
| Z3++-fixedn | 0 | 3201 | 431179.084 | 431045.379 | 3201 | 0 | 3201 | 332 | 8696 | 2023 | 0 |
| 2019-Par4n | 0 | 3079 | 724761.244 | 596837.574 | 3079 | 0 | 3079 | 454 | 8696 | 2628 | 34 |
| z3-4.8.17n | 0 | 2935 | 893397.877 | 893168.293 | 2935 | 0 | 2935 | 598 | 8696 | 2977 | 0 |
| Yices-ismt-fixedn | 0 | 2855 | 1007521.638 | 1007157.359 | 2855 | 0 | 2855 | 678 | 8696 | 998 | 1 |
| Yices-ismt | 0 | 2851 | 973500.001 | 973334.788 | 2851 | 0 | 2851 | 682 | 8696 | 1980 | 1 |
| Yices2 | 0 | 2762 | 976445.186 | 976375.048 | 2762 | 0 | 2762 | 771 | 8696 | 4365 | 0 |
| MathSATn | 0 | 2748 | 1032457.126 | 1032132.542 | 2748 | 0 | 2748 | 785 | 8696 | 3909 | 0 |
| cvc5 | 0 | 2515 | 1321315.279 | 1321235.622 | 2515 | 0 | 2515 | 1018 | 8696 | 3922 | 5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 8410 | 167165.287 | 114362.001 | 8410 | 5594 | 2816 | 3819 | 3785 | 34 |
| Yices2 | 0 | 6817 | 144874.142 | 144696.512 | 6817 | 4349 | 2468 | 5412 | 5412 | 0 |
| Yices-ismt | 0 | 6817 | 145027.615 | 144746.157 | 6817 | 4349 | 2468 | 5412 | 5411 | 1 |
| Yices-ismt-fixedn | 0 | 6815 | 144951.618 | 144754.431 | 6815 | 4347 | 2468 | 5414 | 5413 | 1 |
| Z3++-fixedn | 0 | 6569 | 157870.651 | 157583.735 | 6569 | 3840 | 2729 | 5660 | 5660 | 0 |
| Z3++ | 0 | 6569 | 157966.231 | 157612.653 | 6569 | 3843 | 2726 | 5660 | 5660 | 0 |
| z3-4.8.17n | 0 | 6517 | 164469.19 | 163956.068 | 6517 | 4429 | 2088 | 5712 | 5712 | 0 |
| MathSATn | 0 | 6340 | 169188.477 | 168833.149 | 6340 | 4049 | 2291 | 5889 | 5889 | 0 |
| cvc5 | 0 | 4252 | 210473.191 | 210249.849 | 4252 | 2194 | 2058 | 7977 | 7972 | 5 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.