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 2019-07-23 17:56:09 +0000
Benchmarks: 11494 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 8971 | 6669100.357 | 6217845.833 | 8971 | 6142 | 2829 | 2523 | 2368 | 155 | |
| CVC4 | 0 | 8289 | 9049915.549 | 9312701.246 | 8289 | 5785 | 2504 | 3205 | 3145 | 60 | |
| CVC4-SymBreakn | 0 | 7936 | 10150889.498 | 10253204.123 | 7936 | 5542 | 2394 | 3558 | 3526 | 11 | |
| Yices 2.6.2 | 0 | 7642 | 9539458.61 | 9542887.595 | 7642 | 5106 | 2536 | 3852 | 3852 | 0 | |
| 2018-CVC4n | 0 | 7387 | 10315282.403 | 10412342.718 | 7387 | 5101 | 2286 | 4107 | 4019 | 59 | |
| Z3n | 0 | 5276 | 15583575.037 | 15590828.09 | 5276 | 3344 | 1932 | 6218 | 6010 | 2 | |
| AProVE | 0 | 4165 | 14649432.473 | 17992548.137 | 4165 | 4165 | 0 | 7329 | 7233 | 0 | |
| SMT-RAT | 0 | 1041 | 25111697.825 | 25126644.852 | 1041 | 764 | 277 | 10453 | 10426 | 1 | |
| ProB | 0 | 348 | 19347770.845 | 19461161.617 | 348 | 264 | 84 | 11146 | 7822 | 0 | |
| MathSAT-default | 2 | 8109 | 8843151.29 | 8847791.813 | 8109 | 5564 | 2545 | 3385 | 3382 | 1 | |
| MathSAT-na-ext | 5 | 7892 | 9207941.341 | 9213582.627 | 7892 | 5382 | 2510 | 3602 | 3597 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 9084 | 7001271.317 | 6089981.497 | 9084 | 6229 | 2855 | 2410 | 2255 | 155 | |
| CVC4 | 0 | 8289 | 9304966.749 | 9312543.256 | 8289 | 5785 | 2504 | 3205 | 3145 | 60 | |
| CVC4-SymBreakn | 0 | 7936 | 10246658.578 | 10253017.153 | 7936 | 5542 | 2394 | 3558 | 3526 | 11 | |
| Yices 2.6.2 | 0 | 7642 | 9542876.64 | 9542746.005 | 7642 | 5106 | 2536 | 3852 | 3852 | 0 | |
| 2018-CVC4n | 0 | 7387 | 10408606.763 | 10412159.248 | 7387 | 5101 | 2286 | 4107 | 4019 | 59 | |
| Z3n | 0 | 5276 | 15590372.767 | 15590570.77 | 5276 | 3344 | 1932 | 6218 | 6010 | 2 | |
| AProVE | 0 | 4168 | 18008043.77 | 17992440.437 | 4168 | 4168 | 0 | 7326 | 7230 | 0 | |
| SMT-RAT | 0 | 1041 | 25125565.855 | 25126187.322 | 1041 | 764 | 277 | 10453 | 10426 | 1 | |
| ProB | 0 | 348 | 19370042.845 | 19460928.287 | 348 | 264 | 84 | 11146 | 7822 | 0 | |
| MathSAT-default | 2 | 8109 | 8847365.3 | 8847651.863 | 8109 | 5564 | 2545 | 3385 | 3382 | 1 | |
| MathSAT-na-ext | 5 | 7892 | 9213466.411 | 9213426.977 | 7892 | 5382 | 2510 | 3602 | 3597 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 6229 | 2107070.975 | 1402095.521 | 6229 | 6229 | 0 | 5265 | 2255 | 155 |
| CVC4 | 0 | 5785 | 3642862.147 | 3649537.485 | 5785 | 5785 | 0 | 5709 | 3145 | 60 |
| CVC4-SymBreakn | 0 | 5542 | 4377181.822 | 4383045.536 | 5542 | 5542 | 0 | 5952 | 3526 | 11 |
| Yices 2.6.2 | 0 | 5106 | 4089051.978 | 4088940.878 | 5106 | 5106 | 0 | 6388 | 3852 | 0 |
| 2018-CVC4n | 0 | 5101 | 4399140.536 | 4402593.562 | 5101 | 5101 | 0 | 6393 | 4019 | 59 |
| AProVE | 0 | 4168 | 6701612.37 | 6686020.285 | 4168 | 4168 | 0 | 7326 | 7230 | 0 |
| Z3n | 0 | 3344 | 8761977.162 | 8762119.984 | 3344 | 3344 | 0 | 8150 | 6010 | 2 |
| SMT-RAT | 0 | 764 | 14340413.557 | 14340552.449 | 764 | 764 | 0 | 10730 | 10426 | 1 |
| ProB | 0 | 264 | 11344334.432 | 11378531.281 | 264 | 264 | 0 | 11230 | 7822 | 0 |
| MathSAT-default | 2 | 5564 | 3338667.101 | 3338964.144 | 5564 | 5564 | 0 | 5930 | 3382 | 1 |
| MathSAT-na-ext | 5 | 5382 | 3648017.362 | 3648046.421 | 5382 | 5382 | 0 | 6112 | 3597 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2855 | 516599.873 | 332021.676 | 2855 | 0 | 2855 | 8639 | 2255 | 155 |
| MathSAT-default | 0 | 2545 | 1152698.199 | 1152687.719 | 2545 | 0 | 2545 | 8949 | 3382 | 1 |
| Yices 2.6.2 | 0 | 2536 | 1100224.662 | 1100205.127 | 2536 | 0 | 2536 | 8958 | 3852 | 0 |
| MathSAT-na-ext | 0 | 2510 | 1209449.049 | 1209380.556 | 2510 | 0 | 2510 | 8984 | 3597 | 0 |
| CVC4 | 0 | 2504 | 1308504.602 | 1309405.771 | 2504 | 0 | 2504 | 8990 | 3145 | 60 |
| CVC4-SymBreakn | 0 | 2394 | 1523113.898 | 1523579.486 | 2394 | 0 | 2394 | 9100 | 3526 | 11 |
| 2018-CVC4n | 0 | 2286 | 1662846.555 | 1662930.779 | 2286 | 0 | 2286 | 9208 | 4019 | 59 |
| Z3n | 0 | 1932 | 2693739.823 | 2693733.161 | 1932 | 0 | 1932 | 9562 | 6010 | 2 |
| SMT-RAT | 0 | 277 | 6438298.149 | 6438758.956 | 277 | 0 | 277 | 11217 | 10426 | 1 |
| ProB | 0 | 84 | 4812505.199 | 4845772.492 | 84 | 0 | 84 | 11410 | 7822 | 0 |
| AProVE | 0 | 0 | 7087204.385 | 7087203.018 | 0 | 0 | 0 | 11494 | 7230 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 7994 | 159469.142 | 104683.853 | 7994 | 5374 | 2620 | 3500 | 3345 | 155 | |
| Yices 2.6.2 | 0 | 6539 | 134264.703 | 134175.099 | 6539 | 4209 | 2330 | 4955 | 4955 | 0 | |
| CVC4 | 0 | 5043 | 174751.229 | 174566.816 | 5043 | 3226 | 1817 | 6451 | 6391 | 60 | |
| 2018-CVC4n | 0 | 4982 | 176849.047 | 176667.712 | 4982 | 3182 | 1800 | 6512 | 6453 | 59 | |
| CVC4-SymBreakn | 0 | 4761 | 185243.739 | 185115.45 | 4761 | 3046 | 1715 | 6733 | 6722 | 11 | |
| Z3n | 0 | 3088 | 219342.011 | 219160.752 | 3088 | 1824 | 1264 | 8406 | 8398 | 2 | |
| AProVE | 0 | 3003 | 219126.35 | 211881.334 | 3003 | 3003 | 0 | 8491 | 8395 | 0 | |
| SMT-RAT | 0 | 828 | 257727.345 | 257734.041 | 828 | 583 | 245 | 10666 | 10663 | 1 | |
| ProB | 0 | 290 | 212949.663 | 213016.727 | 290 | 233 | 57 | 11204 | 8493 | 0 | |
| MathSAT-default | 1 | 5932 | 159519.94 | 159330.214 | 5932 | 3916 | 2016 | 5562 | 5560 | 1 | |
| MathSAT-na-ext | 3 | 5855 | 160069.328 | 159897.909 | 5855 | 3868 | 1987 | 5639 | 5636 | 0 |
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.