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 2021-07-18 17:29:07 +0000
Benchmarks: 11683 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 | 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 | 9031 | 3565990.911 | 3284622.517 | 9031 | 6028 | 3003 | 2650 | 2 | 2612 | 38 |
| z3n | 0 | 8662 | 4210270.621 | 4210116.59 | 8662 | 5803 | 2859 | 3021 | 0 | 3012 | 0 |
| MathSAT5n | 0 | 8189 | 4597524.331 | 4597505.153 | 8189 | 5508 | 2681 | 3494 | 0 | 3494 | 0 |
| cvc5 | 0 | 8175 | 4357530.002 | 5123192.635 | 8175 | 5681 | 2494 | 3508 | 0 | 3508 | 0 |
| cvc5 - fixedn | 0 | 8144 | 4344970.834 | 5137972.59 | 8144 | 5651 | 2493 | 3539 | 0 | 3539 | 0 |
| Yices2 | 0 | 7805 | 4828568.419 | 4828706.758 | 7805 | 5113 | 2692 | 3878 | 0 | 3877 | 0 |
| AProVE | 0 | 3996 | 7490983.286 | 9215732.793 | 3996 | 3996 | 0 | 7685 | 2 | 7419 | 0 |
| SMT-RAT | 0 | 2579 | 11164558.249 | 11165896.946 | 2579 | 2287 | 292 | 9104 | 0 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 2570 | 11113832.751 | 11141777.643 | 2570 | 2285 | 285 | 9113 | 0 | 9040 | 13 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 9223 | 3795805.151 | 3162035.509 | 9223 | 6190 | 3033 | 2458 | 2 | 2420 | 38 |
| z3n | 0 | 8662 | 4210810.441 | 4209985.94 | 8662 | 5803 | 2859 | 3021 | 0 | 3012 | 0 |
| MathSAT5n | 0 | 8189 | 4598409.881 | 4597347.663 | 8189 | 5508 | 2681 | 3494 | 0 | 3494 | 0 |
| cvc5 | 0 | 8175 | 5118558.575 | 5123005.685 | 8175 | 5681 | 2494 | 3508 | 0 | 3508 | 0 |
| cvc5 - fixedn | 0 | 8144 | 5132807.469 | 5137768.16 | 8144 | 5651 | 2493 | 3539 | 0 | 3539 | 0 |
| Yices2 | 0 | 7805 | 4829018.099 | 4828578.688 | 7805 | 5113 | 2692 | 3878 | 0 | 3877 | 0 |
| AProVE | 0 | 3998 | 9229598.713 | 9215415.016 | 3998 | 3998 | 0 | 7683 | 2 | 7417 | 0 |
| SMT-RAT | 0 | 2578 | 11165683.129 | 11165546.176 | 2578 | 2286 | 292 | 9105 | 0 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 2570 | 11140755.131 | 11141407.893 | 2570 | 2285 | 285 | 9113 | 0 | 9040 | 13 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 6190 | 1203890.651 | 731342.924 | 6190 | 6190 | 0 | 472 | 5021 | 2420 | 38 |
| z3n | 0 | 5803 | 1451813.723 | 1451305.572 | 5803 | 5803 | 0 | 859 | 5021 | 3012 | 0 |
| cvc5 | 0 | 5681 | 2005636.918 | 2010126.246 | 5681 | 5681 | 0 | 981 | 5021 | 3508 | 0 |
| cvc5 - fixedn | 0 | 5651 | 2019785.503 | 2024780.945 | 5651 | 5651 | 0 | 1011 | 5021 | 3539 | 0 |
| MathSAT5n | 0 | 5508 | 1704489.627 | 1703774.183 | 5508 | 5508 | 0 | 1154 | 5021 | 3494 | 0 |
| Yices2 | 0 | 5113 | 1987386.62 | 1987044.035 | 5113 | 5113 | 0 | 1549 | 5021 | 3877 | 0 |
| AProVE | 0 | 3998 | 3485012.352 | 3470915.682 | 3998 | 3998 | 0 | 2664 | 5021 | 7417 | 0 |
| SMT-RAT | 0 | 2286 | 5503988.333 | 5503836.19 | 2286 | 2286 | 0 | 4376 | 5021 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 2285 | 5500494.608 | 5500862.774 | 2285 | 2285 | 0 | 4377 | 5021 | 9040 | 13 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3033 | 429391.37 | 301159.156 | 3033 | 0 | 3033 | 211 | 8439 | 2420 | 38 |
| z3n | 0 | 2859 | 635693.808 | 635377.215 | 2859 | 0 | 2859 | 387 | 8437 | 3012 | 0 |
| Yices2 | 0 | 2692 | 712765.953 | 712669.123 | 2692 | 0 | 2692 | 554 | 8437 | 3877 | 0 |
| MathSAT5n | 0 | 2681 | 763920.253 | 763573.48 | 2681 | 0 | 2681 | 565 | 8437 | 3494 | 0 |
| cvc5 | 0 | 2494 | 982921.657 | 982879.439 | 2494 | 0 | 2494 | 752 | 8437 | 3508 | 0 |
| cvc5 - fixedn | 0 | 2493 | 983021.966 | 982987.214 | 2493 | 0 | 2493 | 753 | 8437 | 3539 | 0 |
| SMT-RAT | 0 | 292 | 3531694.796 | 3531709.986 | 292 | 0 | 292 | 2954 | 8437 | 9068 | 12 |
| 2020-SMT-RATn | 0 | 285 | 3510260.523 | 3510545.119 | 285 | 0 | 285 | 2961 | 8437 | 9040 | 13 |
| AProVE | 0 | 0 | 3697345.863 | 3697271.491 | 0 | 0 | 0 | 3244 | 8439 | 7417 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 8181 | 159297.647 | 105042.506 | 8181 | 5397 | 2784 | 3500 | 2 | 3462 | 38 |
| Yices2 | 0 | 6825 | 132188.927 | 131978.875 | 6825 | 4423 | 2402 | 4858 | 0 | 4858 | 0 |
| MathSAT5n | 0 | 6319 | 156494.657 | 156013.324 | 6319 | 4076 | 2243 | 5364 | 0 | 5364 | 0 |
| z3n | 0 | 5975 | 163422.9 | 163044.852 | 5975 | 3970 | 2005 | 5708 | 0 | 5703 | 0 |
| cvc5 | 0 | 5838 | 163467.844 | 163002.728 | 5838 | 3746 | 2092 | 5845 | 0 | 5845 | 0 |
| cvc5 - fixedn | 0 | 5837 | 163411.229 | 163082.796 | 5837 | 3744 | 2093 | 5846 | 0 | 5846 | 0 |
| AProVE | 0 | 3056 | 218973.345 | 211486.173 | 3056 | 3056 | 0 | 8625 | 2 | 8359 | 0 |
| 2020-SMT-RATn | 0 | 1652 | 248408.552 | 248312.643 | 1652 | 1405 | 247 | 10031 | 0 | 9996 | 13 |
| SMT-RAT | 0 | 1635 | 249030.248 | 248936.656 | 1635 | 1391 | 244 | 10048 | 0 | 10023 | 12 |
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.