The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_IDL division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 1042 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices 2.6.2 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 938 | 307934.359 | 307947.077 | 938 | 600 | 338 | 104 | 104 | 0 | |
| 2018-Yicesn | 0 | 924 | 319876.37 | 319902.034 | 924 | 597 | 327 | 118 | 118 | 0 | |
| Yices 2.6.2 | 0 | 924 | 321130.895 | 321142.934 | 924 | 597 | 327 | 118 | 118 | 0 | |
| Par4 | 0 | 922 | 335958.888 | 300194.315 | 922 | 591 | 331 | 120 | 120 | 0 | |
| CVC4 | 0 | 875 | 507754.115 | 507685.121 | 875 | 544 | 331 | 167 | 167 | 0 | |
| veriT | 0 | 773 | 784001.654 | 784024.691 | 773 | 453 | 320 | 269 | 269 | 0 | |
| SMTInterpol | 0 | 682 | 974603.494 | 967640.255 | 682 | 386 | 296 | 360 | 360 | 0 | |
| ProB | 0 | 173 | 2086371.547 | 2086495.691 | 173 | 98 | 75 | 869 | 864 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 944 | 410170.698 | 279440.114 | 944 | 607 | 337 | 98 | 98 | 0 | |
| Z3n | 0 | 938 | 307948.649 | 307943.617 | 938 | 600 | 338 | 104 | 104 | 0 | |
| 2018-Yicesn | 0 | 924 | 319895.38 | 319898.304 | 924 | 597 | 327 | 118 | 118 | 0 | |
| Yices 2.6.2 | 0 | 924 | 321146.745 | 321138.774 | 924 | 597 | 327 | 118 | 118 | 0 | |
| CVC4 | 0 | 875 | 507798.585 | 507677.421 | 875 | 544 | 331 | 167 | 167 | 0 | |
| veriT | 0 | 773 | 784036.504 | 784015.531 | 773 | 453 | 320 | 269 | 269 | 0 | |
| SMTInterpol | 0 | 685 | 974645.634 | 967586.655 | 685 | 388 | 297 | 357 | 357 | 0 | |
| ProB | 0 | 173 | 2086466.227 | 2086466.891 | 173 | 98 | 75 | 869 | 864 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 607 | 209742.247 | 121180.361 | 607 | 607 | 0 | 435 | 98 | 0 |
| Z3n | 0 | 600 | 148034.842 | 148029.517 | 600 | 600 | 0 | 442 | 104 | 0 |
| 2018-Yicesn | 0 | 597 | 141972.722 | 141974.908 | 597 | 597 | 0 | 445 | 118 | 0 |
| Yices 2.6.2 | 0 | 597 | 143148.813 | 143151.125 | 597 | 597 | 0 | 445 | 118 | 0 |
| CVC4 | 0 | 544 | 329589.187 | 329521.432 | 544 | 544 | 0 | 498 | 167 | 0 |
| veriT | 0 | 453 | 579254.707 | 579233.841 | 453 | 453 | 0 | 589 | 269 | 0 |
| SMTInterpol | 0 | 388 | 704547.303 | 699904.143 | 388 | 388 | 0 | 654 | 357 | 0 |
| ProB | 0 | 98 | 1313511.332 | 1313510.686 | 98 | 98 | 0 | 944 | 864 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 338 | 90313.807 | 90314.099 | 338 | 0 | 338 | 704 | 104 | 0 |
| Par4 | 0 | 337 | 130828.452 | 88659.753 | 337 | 0 | 337 | 705 | 98 | 0 |
| CVC4 | 0 | 331 | 108609.398 | 108555.99 | 331 | 0 | 331 | 711 | 167 | 0 |
| 2018-Yicesn | 0 | 327 | 108322.659 | 108323.396 | 327 | 0 | 327 | 715 | 118 | 0 |
| Yices 2.6.2 | 0 | 327 | 108397.933 | 108387.649 | 327 | 0 | 327 | 715 | 118 | 0 |
| veriT | 0 | 320 | 135181.797 | 135181.689 | 320 | 0 | 320 | 722 | 269 | 0 |
| SMTInterpol | 0 | 297 | 200498.331 | 198082.511 | 297 | 0 | 297 | 745 | 357 | 0 |
| ProB | 0 | 75 | 703354.894 | 703356.205 | 75 | 0 | 75 | 967 | 864 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 831 | 9699.562 | 6321.822 | 831 | 532 | 299 | 211 | 211 | 0 | |
| 2018-Yicesn | 0 | 818 | 6510.767 | 6511.012 | 818 | 521 | 297 | 224 | 224 | 0 | |
| Yices 2.6.2 | 0 | 817 | 6527.729 | 6516.407 | 817 | 520 | 297 | 225 | 225 | 0 | |
| Z3n | 0 | 761 | 8519.399 | 8508.844 | 761 | 477 | 284 | 281 | 281 | 0 | |
| CVC4 | 0 | 585 | 13471.419 | 13410.875 | 585 | 312 | 273 | 457 | 457 | 0 | |
| veriT | 0 | 501 | 14387.03 | 14385.908 | 501 | 223 | 278 | 541 | 541 | 0 | |
| SMTInterpol | 0 | 439 | 18792.463 | 16451.602 | 439 | 217 | 222 | 603 | 603 | 0 | |
| ProB | 0 | 152 | 21844.916 | 21844.991 | 152 | 94 | 58 | 890 | 887 | 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.