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 2021-07-18 17:29:06 +0000
Benchmarks: 11681 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 9031 | 3565990.911 | 3284622.517 | 9031 | 6028 | 3003 | 2650 | 2612 | 38 |
| z3n | 0 | 8661 | 4209068.947 | 4208914.645 | 8661 | 5803 | 2858 | 3020 | 3011 | 0 |
| MathSAT5n | 0 | 8189 | 4595124.761 | 4595104.923 | 8189 | 5508 | 2681 | 3492 | 3492 | 0 |
| cvc5 | 0 | 8174 | 4356290.797 | 5121953.115 | 8174 | 5681 | 2493 | 3507 | 3507 | 0 |
| cvc5 - fixedn | 0 | 8143 | 4343734.101 | 5136735.447 | 8143 | 5651 | 2492 | 3538 | 3538 | 0 |
| Yices2 | 0 | 7805 | 4826168.739 | 4826306.718 | 7805 | 5113 | 2692 | 3876 | 3875 | 0 |
| AProVE | 0 | 3996 | 7490983.286 | 9215732.793 | 3996 | 3996 | 0 | 7685 | 7419 | 0 |
| SMT-RAT | 0 | 2577 | 11164267.625 | 11165606.258 | 2577 | 2287 | 290 | 9104 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 2568 | 11113579.401 | 11141524.275 | 2568 | 2285 | 283 | 9113 | 9040 | 13 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 9223 | 3795805.151 | 3162035.509 | 9223 | 6190 | 3033 | 2458 | 2420 | 38 |
| z3n | 0 | 8661 | 4209608.517 | 4208784.015 | 8661 | 5803 | 2858 | 3020 | 3011 | 0 |
| MathSAT5n | 0 | 8189 | 4596009.881 | 4594947.663 | 8189 | 5508 | 2681 | 3492 | 3492 | 0 |
| cvc5 | 0 | 8174 | 5117319.15 | 5121766.255 | 8174 | 5681 | 2493 | 3507 | 3507 | 0 |
| cvc5 - fixedn | 0 | 8143 | 5131570.426 | 5136531.077 | 8143 | 5651 | 2492 | 3538 | 3538 | 0 |
| Yices2 | 0 | 7805 | 4826618.099 | 4826178.688 | 7805 | 5113 | 2692 | 3876 | 3875 | 0 |
| AProVE | 0 | 3998 | 9229598.713 | 9215415.016 | 3998 | 3998 | 0 | 7683 | 7417 | 0 |
| SMT-RAT | 0 | 2576 | 11165392.505 | 11165255.488 | 2576 | 2286 | 290 | 9105 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 2568 | 11140501.781 | 11141154.525 | 2568 | 2285 | 283 | 9113 | 9040 | 13 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 6190 | 1203890.651 | 731342.924 | 6190 | 6190 | 0 | 472 | 5019 | 2420 | 38 |
| z3n | 0 | 5803 | 1451813.723 | 1451305.572 | 5803 | 5803 | 0 | 859 | 5019 | 3011 | 0 |
| cvc5 | 0 | 5681 | 2005636.918 | 2010126.246 | 5681 | 5681 | 0 | 981 | 5019 | 3507 | 0 |
| cvc5 - fixedn | 0 | 5651 | 2019785.503 | 2024780.945 | 5651 | 5651 | 0 | 1011 | 5019 | 3538 | 0 |
| MathSAT5n | 0 | 5508 | 1704489.627 | 1703774.183 | 5508 | 5508 | 0 | 1154 | 5019 | 3492 | 0 |
| Yices2 | 0 | 5113 | 1987386.62 | 1987044.035 | 5113 | 5113 | 0 | 1549 | 5019 | 3875 | 0 |
| AProVE | 0 | 3998 | 3485012.352 | 3470915.682 | 3998 | 3998 | 0 | 2664 | 5019 | 7417 | 0 |
| SMT-RAT | 0 | 2286 | 5503988.333 | 5503836.19 | 2286 | 2286 | 0 | 4376 | 5019 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 2285 | 5500494.608 | 5500862.774 | 2285 | 2285 | 0 | 4377 | 5019 | 9040 | 13 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3033 | 429391.37 | 301159.156 | 3033 | 0 | 3033 | 211 | 8437 | 2420 | 38 |
| z3n | 0 | 2858 | 634491.884 | 634175.29 | 2858 | 0 | 2858 | 386 | 8437 | 3011 | 0 |
| Yices2 | 0 | 2692 | 710365.953 | 710269.123 | 2692 | 0 | 2692 | 552 | 8437 | 3875 | 0 |
| MathSAT5n | 0 | 2681 | 761520.253 | 761173.48 | 2681 | 0 | 2681 | 563 | 8437 | 3492 | 0 |
| cvc5 | 0 | 2493 | 981682.233 | 981640.009 | 2493 | 0 | 2493 | 751 | 8437 | 3507 | 0 |
| cvc5 - fixedn | 0 | 2492 | 981784.923 | 981750.132 | 2492 | 0 | 2492 | 752 | 8437 | 3538 | 0 |
| SMT-RAT | 0 | 290 | 3531404.172 | 3531419.298 | 290 | 0 | 290 | 2954 | 8437 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 283 | 3510007.173 | 3510291.751 | 283 | 0 | 283 | 2961 | 8437 | 9040 | 13 |
| AProVE | 0 | 0 | 3697345.863 | 3697271.491 | 0 | 0 | 0 | 3244 | 8437 | 7417 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 8181 | 159297.647 | 105042.506 | 8181 | 5397 | 2784 | 3500 | 3462 | 38 |
| Yices2 | 0 | 6825 | 132140.927 | 131930.875 | 6825 | 4423 | 2402 | 4856 | 4856 | 0 |
| MathSAT5n | 0 | 6319 | 156446.657 | 155965.324 | 6319 | 4076 | 2243 | 5362 | 5362 | 0 |
| z3n | 0 | 5974 | 163396.976 | 163018.927 | 5974 | 3970 | 2004 | 5707 | 5702 | 0 |
| cvc5 | 0 | 5838 | 163419.844 | 162954.728 | 5838 | 3746 | 2092 | 5843 | 5843 | 0 |
| cvc5 - fixedn | 0 | 5837 | 163363.229 | 163034.796 | 5837 | 3744 | 2093 | 5844 | 5844 | 0 |
| AProVE | 0 | 3056 | 218973.345 | 211486.173 | 3056 | 3056 | 0 | 8625 | 8359 | 0 |
| 2020-SMT-RATn | 0 | 1652 | 248360.552 | 248264.643 | 1652 | 1405 | 247 | 10029 | 9994 | 13 |
| SMT-RAT | 0 | 1635 | 248982.248 | 248888.656 | 1635 | 1391 | 244 | 10046 | 10021 | 12 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.